Simple proof of "Diffeomorphism and distance preserving implies isometry" For a Riemannian manifold $(M,g)$, if $F: M\to M$ is a diffeomorphism and preserves distances, I would like to show that $F$ is an isometry. By "distance" I mean $d(x,y)=\inf \int_0^1 |\gamma'(t)| dt$ where the infemum is taken over all admissible curves $\gamma$ (with $\gamma(0)=x$ and $\gamma(1)=y$). By "isometry", I mean that each differential $dF_p : T_p M\to T_{F(p)} M$ is a linear isometry. I know that this is true (at least with mild assumptions on $M$, like possibly connectedness), but I am not sure if there is a "simple" proof of it. For instance, problem 7.7 in Lee's "Introduction to Riemannian Geometry" asks you to show that a homeomorphism that is a metric space isometry is an isometry (so clearly $F$ falls into this category), but the proof is very long. Does anyone know if there is a simple way of showing this? 
 A: Given a minimizing geodesic segment $\gamma : [0,\epsilon] \to M,$ consider the restrictions $$\gamma|_{[0,t]} : [0,t] \to M$$ for small $t$. Each of these is also a minimizing geodesic, and thus we have the inequality
$$\ell_\gamma(t)=L(\gamma|_{[0,t]}) = d(\gamma(0), \gamma(t)) = d(F(\gamma(0)), F(\gamma(t))) \le  L((F\circ\gamma)|_{[0,t]})=\ell_{F\circ\gamma}(t).$$
Since $\ell_\gamma(0) = \ell_{F\circ\gamma}(0) = 0,$ we conclude from calculus that $\ell_{\gamma}'(0) \le \ell_{F \circ \gamma}'(0).$ Since $\ell_\gamma(t) = \int_0^t |\gamma'|,$ we have $\ell_{\gamma}'(t) = |\gamma'(t)|;$ so the inequality of derivatives is $$|\gamma'(0)| \le |(F\circ \gamma)'(0)| = |DF(\gamma'(0))|.$$
By the local existence of geodesics, this implies that $|v|_g \le |DF(v)|_g = |v|_{F^*g}$ for all vectors $v\in TM.$ 
Since $F^{-1}$ is also a distance-preserving diffeomorphism, repeating the same argument with $w = DF(v)$ shows that we also have the opposite inequality $$|v|_g=|DF^{-1}(w)|_g \ge |w|_g = |v|_{F^*g};$$ so in fact we have equality: $$|v|_g = |v|_{F^* g}.$$
By polarization, this equivalence of norms implies the equivalence of inner products; so $g=F^*g$ as desired.
