Q:

Local Inversion theorem (first sentence of the proof)

In this local inversion theorem I want to prove that a map f between two Banach spaces E and F is a local diffeomorphism.
In the proof it says :
Without loss of generality we can consider the case where E= F.
Sorry for this simple question, but why is that? How does this imply the general case where f goes from an open set U in E to F? 
In finite dimensions we could probably have an embedding of E in F or something similar...but I'm not sure how to justify this for general Banach spaces...

A:

Just so we're on the same page, regarding notation etc I'll state the IFT:

Inverse Function Theorem:
Let $E,F$ be real Banach spaces, $f:E \to F$ be a $C^k$ map such that at a point $x_0 \in E$, the differential $df_{x_0}$ is an invertible element of $L(E,F)$. Then, there is an open set $U \subset E$ containing $x_0$, an open set $V \subset F$ containing $f(x_0)$, such that $f:U \to V$ is invertible. The inverse map $f^{-1}:V \to U$ is also $C^k$,
.... (now they give a formula for the derivative of the inverse)

Suppose now that we manage to prove this theorem in the case where the domain and target space of the function are both $E$. We are now going to deduce it in the general case as follows: with notation as in the theorem, define a new map
\begin{equation}
g = (df_{x_0})^{-1} \circ f
\end{equation}
Notice that it maps $E$ into $E$. Since $f$ is $C^k$, and $(df_{x_0})^{-1}$ is an element of $L(F,E)$ , it is $C^{\infty}$. Hence $g$ being the composition is atleast $C^k$. A simple computation shows (use chain rule)
\begin{align}
dg_{x_0} = \text{id}_E \tag{*}
\end{align}
So, $dg_{x_0}$ is an invertible element of $L(E,E)$. Now all the relevant hypotheses on $g$ are satisfied. So, by the special case, we know that there an open set $U \subset E$ containing $x_0$, an open subset $W$ containing $g(x_0)$, such that $g: U \to W$ is $C^k,$ with $C^k$ inverse $g^{-1}: W \to U$.
Now notice that by definition, $f = df_{x_0} \circ g$. So, if we take $V = f[U]$, then $f:U \to V$ is a composition of invertible maps, it is also invertible, with $f^{-1} = g^{-1} \circ (df_{x_0})^{-1}$, which is also a composition of $C^k$ maps, and hence $f^{-1}$ is $C^k$. This proves the simplification is sufficient.

Extra Remarks:

Notice that by $(*)$, we may also assume that $df_{x_0} = \text{id}_E$.
One result which I implicitly made use of above is Banach's Isomorphism theorem, which states that if $T: E \to F$ is a linear and continuous (equivalently, bounded) map (which by definition is what it means to be an element of $L(E,F)$) which is invertible, then the inverse $T^{-1}:F \to E$ is guranteed to be continuous (equivalently bounded), so that $T^{-1}$ is in $L(F,E)$. Continuity and linearity then immediately implies both are $C^{\infty}$. In finite dimensions this is obvious, because every linear map between finite-dimensional spaces is continuous, but apparently it's a hard theorem in infinite dimensions.

