Inverse mapping theorem over a complete non-archimedean field

Let $K$ be a complete field with respect to a non-trivial non-archimedean absolute value $|\cdot|$. Let $E$ be a vector space over $K$. A norm $||\cdot||$ on $E$ is a map $E \rightarrow \mathbb{R}$ satisfying the following properties.

1) $||x|| = 0$ if and only if $x = 0$.

2) $||\alpha x|| = |\alpha|||x||$ for all $\alpha \in K$ and all $x \in E$.

3) $||x + y|| \le max(||x||, ||y||)$ for all $x, y \in E$.

Clearly $||x - y||$ defines a metric on $E$. A vector space over $K$ equipped with a norm is called a normed vector space. If $E$ is complete with respect to this metric, $E$ is called a Banach space.

Let $E, F$ be normed vector spaces over $K$. Let $U$ be an open subset of $E$. Let $a \in U$. Let $f\colon U \rightarrow F$ be a map. Suppose there exists a continuous linear map $L\colon E \rightarrow F$ such that $$\frac {||f(x) - f(y) - L(x - y)||}{||x - y||} \rightarrow 0$$ when $(x, y) \rightarrow (a, a)$. Then $f$ is called strictly differentiable at $a$. It is easy to see that $L$ is uniquely determined by $f$ and $a$. We denote $L$ by $Df(a)$.

The following proposition is stated without a proof in Bourbaki, Variete differentielles et analytiques. How do we prove it?

Proposition Let $E, F$ be Banach spaces over $K$. Let $U$ be an open subset of $E$. Let $a \in U$. Let $f\colon U \rightarrow F$ be a map. Suppose $f$ is strictly differentiable at $a$ and $Df(a)$ is an isomorphism $E \rightarrow F$. Then there exist an open neighborhood $U_0$ of $a$ such that $U_0 \subset U$ and an open neighborhood $V_0$ of $f(a)$ with the following properties.

1) $f|U_0$ is a homeomorphism $U_0 \rightarrow V_0$.

2) Let $g$ be the inverse of $f|U_0$. Then $g$ is strictly differentiable at $f(a)$.

3) $Dg(f(a)) = Df(a)^{-1}$.

• What have you tried? For example, how might a proof over the reals fail for the $p$-adics? – Andrew Oct 23 '12 at 1:22
• Actually, have you tried this book: books.google.ca/… – Andrew Oct 23 '12 at 1:33
• @Andrew No. Does the book treat Banach spaces over a non-archimedean field? – Makoto Kato Oct 23 '12 at 1:37
• It treats Banach spaces over $\Bbb R,$ but I thought that maybe the proof could be tweaked to work more generally. – Andrew Oct 23 '12 at 1:56