[proofplan] Let $G: N \to M$ denote the smooth inverse map $F^{-1}$. Since $G \circ F = \operatorname{id}_M$ and $F \circ G = \operatorname{id}_N$, the [chain rule for differentials](/theorems/3907) turns these two identities of smooth maps into two identities of linear maps on tangent spaces. These identities show that $dG_{F(p)}$ is both a left and right inverse for $dF_p$, so $dF_p$ is a linear isomorphism. [/proofplan]

[step:Introduce the smooth inverse and the relevant tangent maps] Fix a point $p \in M$, and define $q := F(p) \in N$. Since $F: M \to N$ is a diffeomorphism, it is bijective, smooth, and its inverse map \begin{align*} G := F^{-1}: N \to M \end{align*} is smooth. The differential of $F$ at $p$ is the [linear map](/page/Linear%20Map) \begin{align*} dF_p: T_pM \to T_qN. \end{align*} The differential of $G$ at $q$ is the linear map \begin{align*} dG_q: T_qN \to T_{G(q)}M. \end{align*} Because $q = F(p)$ and $G = F^{-1}$, we have $G(q) = p$, so this becomes \begin{align*} dG_q: T_qN \to T_pM. \end{align*} [/step]

[step:Apply the chain rule to the two inverse identities]The inverse identities for $F$ and $G$ are \begin{align*} G \circ F = \operatorname{id}_M \end{align*} and \begin{align*} F \circ G = \operatorname{id}_N. \end{align*} Both compositions are smooth because $F$ and $G$ are smooth. Applying the chain rule for differentials to $G \circ F: M \to M$ at $p$ gives \begin{align*} d(G \circ F)_p = dG_{F(p)} \circ dF_p. \end{align*} Since $G \circ F = \operatorname{id}_M$, the differential of the left-hand side is \begin{align*} d(G \circ F)_p = d(\operatorname{id}_M)_p = \operatorname{id}_{T_pM}. \end{align*} Therefore \begin{align*} dG_q \circ dF_p = \operatorname{id}_{T_pM}. \end{align*} Applying the chain rule for differentials to $F \circ G: N \to N$ at $q$ gives \begin{align*} d(F \circ G)_q = dF_{G(q)} \circ dG_q. \end{align*} Since $G(q) = p$ and $F \circ G = \operatorname{id}_N$, we obtain \begin{align*} dF_p \circ dG_q = \operatorname{id}_{T_qN}. \end{align*}[/step]

[guided]We now turn the statement that $F$ and $G$ are inverse maps into a statement about their differentials. The two inverse identities are identities of smooth maps: \begin{align*} G \circ F = \operatorname{id}_M \end{align*} and \begin{align*} F \circ G = \operatorname{id}_N. \end{align*} The chain rule for differentials applies because $F$ and $G$ are smooth maps between smooth manifolds. Applying it to the composition $G \circ F: M \to M$ at the point $p$ gives \begin{align*} d(G \circ F)_p = dG_{F(p)} \circ dF_p. \end{align*} But $G \circ F$ is exactly the identity map on $M$. The differential of the identity map at $p$ is the identity linear map on $T_pM$, so \begin{align*} d(G \circ F)_p = d(\operatorname{id}_M)_p = \operatorname{id}_{T_pM}. \end{align*} Combining the two displayed identities gives \begin{align*} dG_{F(p)} \circ dF_p = \operatorname{id}_{T_pM}. \end{align*} Since $q$ was defined by $q := F(p)$, this is \begin{align*} dG_q \circ dF_p = \operatorname{id}_{T_pM}. \end{align*} We also need the reverse composition, because a two-sided inverse is what proves that a linear map is an isomorphism. Apply the chain rule to the composition $F \circ G: N \to N$ at the point $q \in N$. This gives \begin{align*} d(F \circ G)_q = dF_{G(q)} \circ dG_q. \end{align*} Since $G(q) = p$ and $F \circ G = \operatorname{id}_N$, the left-hand side is the identity linear map on $T_qN$. Hence \begin{align*} dF_p \circ dG_q = \operatorname{id}_{T_qN}. \end{align*} Thus $dG_q$ is simultaneously a left inverse and a right inverse for $dF_p$.[/guided]

[step:Conclude that the differential is a linear isomorphism] We have shown that the linear maps \begin{align*} dF_p: T_pM \to T_qN \end{align*} and \begin{align*} dG_q: T_qN \to T_pM \end{align*} satisfy \begin{align*} dG_q \circ dF_p = \operatorname{id}_{T_pM} \end{align*} and \begin{align*} dF_p \circ dG_q = \operatorname{id}_{T_qN}. \end{align*} Therefore $dG_q$ is the inverse linear map of $dF_p$. Hence $dF_p$ is a linear isomorphism from $T_pM$ to $T_{F(p)}N$. Since $p \in M$ was arbitrary, the result holds for every $p \in M$. [/step]