A transverse Banach bundle section has a split zero submanifold

Let $p$ be a zero of $s$ and let $\mathrm{\Phi }$ be a smooth local trivialization over an open neighbourhood $U$ of $p$; then $\sigma :={\mathrm{pr}}_2\circ \mathrm{\Phi }\circ s:U\to F$ is smooth and ${\sigma }^{-1}(0)=s^{-1}(0)\cap U$. For every $q\in {\sigma }^{-1}(0)$, [L1] identifies $D\sigma (q):T_{q}U\to F$ with $D^{v}s(q)$ followed by the fibre isomorphism ${\mathrm{\Phi }}_q:{\mathcal{E}}_q\to F$. Thus $D\sigma (q)$ is surjective with complemented kernel for every point of this local zero set. The atlas on $U$ formed by restrictions of charts of the maximal smooth atlas on $M$ is itself maximal: every compatible smooth chart on $U$ is also compatible with the atlas of $M$ (charts not meeting its domain are automatically compatible), and hence already belongs to that atlas.

Apply [L2] with $k=\mathrm{\infty }$ to the smooth map $\sigma :U\to F$ at the value $0$. The domain carries the maximal smooth atlas verified in [step 1.1], and every point of ${\sigma }^{-1}(0)$ has derivative onto with complemented kernel. Therefore ${\sigma }^{-1}(0)$ is a split smooth submanifold of $U$ and $T_q({\sigma }^{-1}(0))=\ker D\sigma (q)$ for every $q\in {\sigma }^{-1}(0)$.

Since $U$ is open in $M$, the set ${\sigma }^{-1}(0)=s^{-1}(0)\cap U$ is a split submanifold of $M$ as well, with the same tangent spaces: splitness is local by [L3] and the local charts of $U$ are charts of $M$.

The zeros of $s$ are covered by such neighbourhoods $U$ as $p$ ranges over $s^{-1}(0)$; by [step 3.1] each point of $s^{-1}(0)$ has a split chart in $M$, so $s^{-1}(0)$ is a split smooth submanifold of $M$.

For the tangent description, fix a zero $p$ and two trivializations $\mathrm{\Phi }$ over $U$ and $\mathrm{\Psi }$ over $V$ with $p\in U\cap V$, and let ${\sigma }_{\mathrm{\Phi }},{\sigma }_{\mathrm{\Psi }}$ be the corresponding local representatives; [L1] gives $D{\sigma }_{\mathrm{\Psi }}(p)=g(p)D{\sigma }_{\mathrm{\Phi }}(p)$, where $g(p)$ is the invertible fibre isomorphism of the cocycle. Hence the kernels of $D{\sigma }_{\mathrm{\Psi }}(p)$ and $D{\sigma }_{\mathrm{\Phi }}(p)$ coincide, and the kernel of $D^{v}s(p)$ is intrinsically characterised as the set of $\xi \in T_{p}M$ with $D{\sigma }_{\mathrm{\Phi }}(p)\xi =0$ for one, equivalently every, trivialization around $p$.

Combining [step 2.1] with [step 4.2]: for a zero $p$, $T_p(s^{-1}(0))=\ker D{\sigma }_{\mathrm{\Phi }}(p)=\ker D^{v}s(p)$, the first equality because ${\sigma }^{-1}(0)$ is the zero set of the local representative and the tangent of a split submanifold is computed in its charts, the second by the trivialization-independence just proved.