I'm having trouble understanding a crutial step in the IFT proof for banach spaces.
The theorem is stated as follows
Theorem: Let $E_1,E_2,F$ be Banach spaces and let $\Omega\subseteq E_1, \mho\subseteq E_2$ be open sets.
Let $f:\Omega\times \mho\to F$ be of class $C^1$ and suppose that there is $(x_0,y_0)\in \Omega\times\mho$ such that $D_yf(x_0,y_0):E_2\to F$ is an isomorphism and put $f(x_0,y_0)=z_0$.
Then, there exist open neighborhoods $U\subseteq \Omega$ of $x_0$ and $V\subseteq F$ of $z_0$ and a $C^1$ function $\varphi:U\times V\to \mho$ such that for all $(x,z)\in U\times V$ we have $f(x,\varphi(x,z))=z$.
In the class notes I have a proof that begins as follows
Proof: Let $H:\Omega\times \mho\to E_1\times F$ be defined by $H(x,y)=(x,f(x,y))$. $H$ is $C^1$ as each of its components is $C^1$. By the total derivative formula we know its differential is $$DH(x_0,y_0)(x,y)=(Did(x),Df(x_0,y_0)(x,y))=(x,D_xf(x_0,y_0)(x)+D_yf(x_0,y_0)(y))$$ and this is an isomorphism between the Banach spaces $E_1\times E_2$ and $E_1\times F$, thus by the inverse function theorem...
My question is why is $DH(x_0,y_0)(x,y)$ an isomorphism?
I know it suffices to prove that the second component $(x,y)\mapsto D_xf(x_0,y_0)(x)+D_yf(x_0,y_0)(y)$ is an isomorphism.
I can prove that it is linear and suryective but it doesn't seem clear at all why it should be invertible since all we know is that $y\mapsto D_yf(x_0,y_0)(y)$ is.
Any help is appreciated.
Put $a = (x_0,y_0)$, and I'll write the partial differentials as $D_1f_a$ for what you've written $D_xf(x_0,y_0)$ etc. By what you wrote, we have for all $(u,v)\in E_1\times E_2$, \begin{align} DH_a(u,v) &= (u, D_1f_a(u) + D_2f_a(v)) \end{align} If we call this output $(\xi,\eta)$, then we have the equations \begin{align} \begin{cases} \xi &= u \\ \eta &= D_1f_a(u) + D_2f_a(v) \end{cases} \end{align} This system of equations can easily be inverted to express $u,v$ in terms of $\xi,\eta$ as follows: \begin{align} \begin{cases} u &= \xi \\ v &= (D_2f_a)^{-1}[\eta - D_1f_a(\xi)] \end{cases} \end{align} where by hypothesis, $D_2f_a:E_2 \to F$ is an isomorphism which is why we can invert it. In other words, the map $DH_a$ is invertible, and its inverse is the map $E_1\times F \to E_1\times E_2$ given by \begin{align} (\xi,\eta) &\mapsto \bigg(\xi, (D_2f_a)^{-1}[\eta - D_1f_a(\xi)]\bigg). \end{align}
By the way, your reasoning
isn't right. I mean sure, it would suffice to prove this, but it turns out this assertion is false. Note that this is a mapping $E_1\times E_2\to F$, so even in the finite-dimensional case (because $E_2\cong F$), we're mapping from a higher-dimensional space to a lower-dimensional space, so it's impossible for this map to be an isomorphism. At best, it is going to be surjective.
The entire purpose of "enlarging the target space" by introducing the mapping $H:E_1\times E_2 \to E_1\times F$ is to ensure that (its derivative is) a mapping between spaces which are isomorphic. So, if you completely disregard the role played by the $E_1$ in $E_1\times F$, then it means you're thinking of the situation incorrectly.