# 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?

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.