Theorem: Let $\phi:M_1 \to M_2$ a differentiable application on n-dimensional manifolds and $p \in M_1$ such that $d\phi_p:T_pM_1 \to T_{\phi(p)}M_2$ is an isomorphism. Then $\phi$ is a local diffeomorphism.
The autor says it is a direct apllication of Inverse Function Theorem, but why?
If $\phi$ is differentiable I have that $y^{-1}\circ\phi\circ x: U \subset_{\rm{open}}\mathbb{R^n} \to \mathbb{R}^m$ is differentiable, then if I had $d(y^{-1}\circ\phi\circ x)_p$ isomorphism I could use IFT and say $y^{-1}\circ\phi\circ x$ is a local diffeomorphism, but the information I have is about $d\phi_p$, not $d(y^{-1}\circ\phi\circ x)_p$. Am I supposed to use some kind of chain rule here? Because that would be odd, since the autor didn't define chain rule for functions on manifolds yet...
Thanks.
We are dealing with manifolds, and we should convert all mappings and differentials between manifolds to those between open sets in Euclidean space. You've given that $\mathrm d\varphi_p$ is an isomorphism, then by choosing charts [or parametrization as M. do Carmo used] $\mathrm d\varphi_p$ is totally characterized by $\mathrm d(y^{-1} \circ \varphi \circ x)_{x^{-1}(p)}$ by definition, which is the differential of a mapping between $\mathbb R^n$ and $\mathbb R^n$. So equivalently you are given that $\mathrm d(y^{-1}\circ \varphi \circ x)_{x^{-1}(p)}\colon \mathbb R^n \to \mathbb R^n$ is an isomorphism. Now apply IFT to $(y^{-1}\circ \varphi \circ x)$.
Thus we have a local diffeomorphism $\alpha \colon U \to \alpha (U)$. From now on, no chain rules needed: $\alpha $ and $\alpha^{-1}$ are invertible and differentiable. Use this we construct $$ \psi : =y \circ \alpha \circ x^{-1} \colon x(U) \to y^{-1}(\alpha (U)). $$ This is differentiable by definition: $y^{-1} \circ \psi \circ x = \alpha $ as we shown above. Also it is invertible since $x \circ \alpha^{-1} \circ y^{-1} =: \psi^{-1}$ is a composition of bijections. This inverse $\psi^{-1}$ is differentiable since $x^{-1} \circ \psi^{-1} \circ y = \alpha^{-1}$ is.