Banach manifold differentials are chart independent

(Reflexivity and symmetry.) For a chart $\phi$ at $p$ the transition $\phi \circ {\phi }^{-1}$ is the identity on an open set containing $\phi (p)$, so $D(\phi \circ {\phi }^{-1})(\phi (p))=I$ by [L2] and $(\phi ,v)\sim (\phi ,v)$. If $(\phi ,v)\sim (\psi ,w)$, then $w=D(\psi \circ {\phi }^{-1})(\phi (p))v$; the two transition maps are mutually inverse $C^1$ maps on neighbourhoods of $\phi (p)$ and $\psi (p)$, so differentiating the identities $(\phi \circ {\psi }^{-1})\circ (\psi \circ {\phi }^{-1})=\mathrm{i}\mathrm{d}$ and $(\psi \circ {\phi }^{-1})\circ (\phi \circ {\psi }^{-1})=\mathrm{i}\mathrm{d}$ with [L2] gives $D(\phi \circ {\psi }^{-1})(\psi (p))w=v$, that is $(\psi ,w)\sim (\phi ,v)$.

(Transitivity.) If $(\phi ,v)\sim (\psi ,w)$ and $(\psi ,w)\sim (\chi ,u)$, then on a neighbourhood of $\phi (p)$ the identity $\chi \circ {\phi }^{-1}=(\chi \circ {\psi }^{-1})\circ (\psi \circ {\phi }^{-1})$ holds, and [L2] gives $D(\chi \circ {\phi }^{-1})(\phi (p))v=D(\chi \circ {\psi }^{-1})(\psi (p))D(\psi \circ {\phi }^{-1})(\phi (p))v=D(\chi \circ {\psi }^{-1})(\psi (p))w=u$, that is $(\phi ,v)\sim (\chi ,u)$. Together with [step 1.1], this establishes the equivalence relation before any construction is asserted on its classes.

(The differential is well defined.) Let $f:M\to N$ be $C^1$ and let $(\phi ,\psi )$, $({\phi }^{\mathrm{\prime }},{\psi }^{\mathrm{\prime }})$ be two chart pairs at $p$ and $f(p)$. On a neighbourhood of ${\phi }^{\mathrm{\prime }}(p)$ one has ${\psi }^{\mathrm{\prime }}\circ f\circ {\phi }^{\mathrm{\prime }-1}=({\psi }^{\mathrm{\prime }}\circ {\psi }^{-1})\circ (\psi \circ f\circ {\phi }^{-1})\circ (\phi \circ {\phi }^{\mathrm{\prime }-1})$; if $({\phi }^{\mathrm{\prime }},v^{\mathrm{\prime }})\sim (\phi ,v)$, that is $v=D(\phi \circ {\phi }^{\mathrm{\prime }-1})({\phi }^{\mathrm{\prime }}(p))v^{\mathrm{\prime }}$, then [L2] gives $D({\psi }^{\mathrm{\prime }}\circ f\circ {\phi }^{\mathrm{\prime }-1})({\phi }^{\mathrm{\prime }}(p))v^{\mathrm{\prime }}=D({\psi }^{\mathrm{\prime }}\circ {\psi }^{-1})(\psi (f(p)))[D(\psi \circ f\circ {\phi }^{-1})(\phi (p))v]$, which is precisely the relation $[{\psi }^{\mathrm{\prime }},D({\psi }^{\mathrm{\prime }}\circ f\circ {\phi }^{\mathrm{\prime }-1})({\phi }^{\mathrm{\prime }}(p))v^{\mathrm{\prime }}]=[\psi ,D(\psi \circ f\circ {\phi }^{-1})(\phi (p))v]$ defining $\sim$ on the target manifold. Because [step 1.1] and [step 2.1] have already proved that $\sim$ is an equivalence relation, this comparison proves independence of both the representative and the chart pair.

(The vector space operations are chart independent.) If $(\phi ,v)\sim ({\phi }^{\mathrm{\prime }},v^{\mathrm{\prime }})$ and $(\phi ,w)\sim ({\phi }^{\mathrm{\prime }},w^{\mathrm{\prime }})$, then the shared transition derivative $T:=D({\phi }^{\mathrm{\prime }}\circ {\phi }^{-1})(\phi (p))$ is linear with $v^{\mathrm{\prime }}=Tv$, $w^{\mathrm{\prime }}=Tw$; hence $v^{\mathrm{\prime }}+w^{\mathrm{\prime }}=T(v+w)$ and $\lambda v^{\mathrm{\prime }}=T(\lambda v)$, that is $(\phi ,v+w)\sim ({\phi }^{\mathrm{\prime }},v^{\mathrm{\prime }}+w^{\mathrm{\prime }})$ and $(\phi ,\lambda v)\sim ({\phi }^{\mathrm{\prime }},\lambda v^{\mathrm{\prime }})$. Since $\sim$ is an equivalence relation by [step 1.1] and [step 2.1], these representative calculations define operations on the quotient classes.

(Functoriality.) The maps in this step are well defined on tangent classes by [step 3.1]. For the identity, $D({\mathrm{i}\mathrm{d}}_M)(p)[\phi ,v]=[\phi ,D(\phi \circ {\mathrm{i}\mathrm{d}}_M\circ {\phi }^{-1})(\phi (p))v]=[\phi ,D(\mathrm{i}\mathrm{d})(\phi (p))v]=[\phi ,v]$ by [L2]. For a composite, fix charts $\phi$ at $p$, $\psi$ at $f(p)$ and $\rho$ at $g(f(p))$; then $\rho \circ (g\circ f)\circ {\phi }^{-1}=(\rho \circ g\circ {\psi }^{-1})\circ (\psi \circ f\circ {\phi }^{-1})$ near $\phi (p)$, and applying [L2] to this identity of open-subset maps gives equality of the two well-defined maps $D(g\circ f)(p)$ and $Dg(f(p))\circ Df(p)$ on every class represented in the chart $\phi$.

Assertion 1 is [step 1.1] with [step 2.1]; assertion 2 is [step 3.1] and [step 3.2]; assertion 3 is [step 4.1].