Regular value theorem for Banach manifolds

Fix $p\in S:=f^{-1}(q)$ and choose specified-atlas charts ${\phi }_0:U\to E$ of $M$ at $p$ and $\psi :V\to F$ of $N$ at $q$. Put $a:={\phi }_0(p)$ and $b:=\psi (q)$. The translated coordinate map $\phi :={\phi }_0-a$ is a $C^k$ chart compatible with the specified atlas of $M$; maximality therefore makes $\phi$ a chart of the structured manifold, and $\phi (p)=0$. Writing $L:=Df(p)$, the recentered coordinate representative $\widehat{f}(x):=\psi (f({\phi }^{-1}(x)))-b$ is $C^k$ on the open set $\mathrm{\Omega }:=\phi [U\cap f^{-1}[V]]\subseteq E$, satisfies $\widehat{f}(0)=0$, and has $D\widehat{f}(0)=D\psi (q)\circ L\circ D\phi (p{)}^{-1}\mathrm{.}$ Translations have identity derivative, so this follows from chart functoriality and the chain rule without requiring a translated target chart to belong to the atlas of $N$.

The kernel of $D\widehat{f}(0)$ is $K:=D\phi (p)[\ker L]$, a complemented subspace of $E$: the chart derivative $D\phi (p)$ is a bounded linear isomorphism by [L1] and [L5] applied to $\phi \circ {\phi }^{-1}=\mathrm{i}\mathrm{d}$, and [L4] transports the given complement of $\ker L$ to a complement of $K$; moreover $D\widehat{f}(0)$ is surjective, because $D\psi (q)$ and $D\phi (p)$ are isomorphisms and $L$ is onto.

Fix a topological direct sum $E=K\oplus E_1$ with bounded projections $P_K$, $P_{E_1}$ existing by [step 2.1] and [L4], and let $L_1:=D\widehat{f}(0){\mathrm{\mid }}_{E_1}:E_1\to F$. Then $L_1$ is a bounded linear bijection: it is injective because $\ker D\widehat{f}(0)=K$ meets $E_1$ only in $0$, and surjective because $D\widehat{f}(0)$ is onto and agrees with $L_1$ on $E_1$; hence $L_1^{-1}$ is bounded by [L3] and AC supplies the DC that [L3] assumes.

Define $G:{\mathrm{\Omega }}^{\mathrm{\prime }}\to F$ on the open set ${\mathrm{\Omega }}^{\mathrm{\prime }}:=\{(w,u)\in K\times E_1:w+u\in \mathrm{\Omega }\}$ by $G(w,u):=\widehat{f}(w+u)$. Then $G$ is $C^k$, $G(0,0)=0$, and its partial derivative in the second variable at $(0,0)$ is $L_1$, a bounded linear isomorphism by [step 3.1]; by [L2] there are open neighbourhoods $A\subseteq K$ of $0$ and $B\subseteq E_1$ of $0$ and a $C^k$ map $h:A\to B$ with $\{(w,u)\in A\times B:\widehat{f}(w+u)=0\}=\{(w,h(w)):w\in A\}\mathrm{.}$

The map $\mathrm{\Theta }(w,u):=(w,u-h(w))$ is a homeomorphism of $A\times E_1$ onto itself with inverse $(w,v)\mapsto (w,v+h(w))$, and both maps are $C^k$. It carries the zero set $\{(w,h(w)):w\in A\}$ of [step 4.1] onto the slice $A\times \{0\}$. Let $U_1:={\phi }^{-1}(A\times B)$ and define $\mathrm{\Phi }:=\mathrm{\Theta }\circ \phi {\mathrm{\mid }}_{U_1}$. Its image $\mathrm{\Theta }(A\times B)$ is open, and $\mathrm{\Phi }$ is a $C^k$ chart compatible with every specified-atlas chart $\chi$: on each overlap the two transitions are $\mathrm{\Phi }\circ {\chi }^{-1}=\mathrm{\Theta }\circ \phi \circ {\chi }^{-1},\chi \circ {\mathrm{\Phi }}^{-1}=\chi \circ {\phi }^{-1}\circ {\mathrm{\Theta }}^{-1},$ restricted to open domains, hence are $C^k$. Maximality of the specified atlas of $M$ now implies that $\mathrm{\Phi }$ is a chart of the structured manifold. Finally, $\mathrm{\Phi }[U_1\cap S]=\mathrm{\Phi }[U_1]\cap (K\oplus \{0\}),$ so $\mathrm{\Phi }$ is the split chart required by the library definition.

In the charts $\mathrm{\Phi }$ and $\psi$ of [step 5.1], the coordinate representative of $f$ is $b+\widehat{f}\circ {\mathrm{\Theta }}^{-1}$; its derivative at $0$ is $D\widehat{f}(0)\circ D\mathrm{\Theta }(0{)}^{-1}=D\widehat{f}(0)$ because $D\mathrm{\Theta }(0)=I$. Indeed, $h(0)=0$ and $Dh(0)=0$, the latter by differentiating $G(w,h(w))=0$ at $w=0$ with [L5], which gives $D_{K}G(0,0)+L_{1}Dh(0)=0$ and $D_{K}G(0,0)=D\widehat{f}(0){\mathrm{\mid }}_K=0$. Consequently the kernel of the differential of $f$ at $p$, computed in the charts $\mathrm{\Phi }$ and $\psi$, is exactly the set of classes $[\mathrm{\Phi },k]$ with $k\in K$, which by [step 5.1] is the tangent space of $S$ at $p$; hence $T_{p}S=\ker Df(p)$.

Since $p\in S$ was arbitrary, [step 5.1] gives a split chart for $S$ at every one of its points, so $S$ is a split $C^k$ submanifold of $M$, and [step 6.1] identifies its tangent space at each $p\in S$ with $\ker Df(p)$.