I was checking the proof of Hilbert's theorem in do Carmo's book and got stuck in the following proposition:
If $\psi: S\to \mathbb{R}^3$ is an isometric immersion of an abstract surface $S$ with constant and negative Gaussian curvature, then $\phi = \psi\circ\operatorname{exp}_p:S'\to\mathbb{R}^3$ is also an isometric immersion.
Here the surface $S'$ is just the plane $T_pS$ endowed with the metric induced by the local diffeomorphism $\operatorname{exp}_p:T_pS\to S$.
The problem I'm having is to show that $\phi$ is an isometry. Note, by using that $\psi$ is an isometry, we have that
\begin{align*} \langle d\phi_v(u),d\phi_v(w) \rangle &= \langle d\psi_{\operatorname{exp}_pv}d({\operatorname{exp}_p})_v(u),d\psi_{\operatorname{exp}_pv}d({\operatorname{exp}_p})_v(w)\rangle \\ &= \langle d({\operatorname{exp}_p})_v(u),d({\operatorname{exp}_p})_v(w)\rangle. \end{align*}
By some lemma in do Carmo's, we have the inequality
$$ \langle d({\operatorname{exp}_p})_v(u),d({\operatorname{exp}_p})_v(u)\rangle\geq \langle u,u\rangle. $$
I wonder if there is any simple proof since the author doesn't even comment it. The same happens in the Wikipedia page of Hilbert's theorem, first paragraph of the proof section.
Thanks in advance for any replies.