Understanding why I can apply Inverse Function Theorem to Manifolds. 
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.
 A: 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. 
