Riemannian isometries preserve length and distance

Given: An isometry $F:(M,g)\to (N,h)$.

Riemannian isometry and local isometry: An isometry $F:(M,g)\to (N,h)$ is a diffeomorphism with $F^{\ast }h=g$. A local isometry is a smooth local diffeomorphism with $F^{\ast }h=g$. An isometric immersion is a smooth immersion satisfying that same pullback identity. Use def-pullback-riemannian-metric and def-diffeomorphism-and-local-diffeomorphism-of-manifolds. Positivity forces injective differential by prop-pullback-of-a-riemannian-metric-is-riemannian-exactly-for-immersions. In equal dimensions on boundaryless manifolds, the inverse function theorem as applied in the next proposition makes a metric-preserving smooth map a local isometry. At a boundary the definition retains the local-diffeomorphism requirement. An isometric immersion need not have equal source and target dimensions.

A smooth map with pointwise operator norm at most c is c lipschitz for riemannian distance: Let $M,N$ be connected Riemannian manifolds. If smooth $F:M\to N$ satisfies $\mathrm{\mid }d{F}_{p}v{\mathrm{\mid }}_h\le c\mathrm{\mid }v{\mathrm{\mid }}_g$ for a finite $c\ge 0$ and all $p,v$, then $d_h(Fp,Fq)\le c{d}_g(p,q)$.

Riemannian speed and length: The Riemannian speed on a $C^1$ piece is $\mathrm{\mid }\dot{\gamma }(t){\mathrm{\mid }}_g=\sqrt{g_{\gamma (t)}(\dot{\gamma }(t),\dot{\gamma }(t))}$. Its length is $L_g(\gamma )={\sum }_j{\int }_{t_{j-1}}^{t_j}\mathrm{\mid }\dot{\gamma }(t){\mathrm{\mid }}_{g}dt$. The curve convention is def-piecewise-c-one-curve-on-a-manifold and the norm is def-pointwise-norm-and-angle-from-a-riemannian-metric. Each integrand is continuous on its closed piece with the one-sided endpoint derivative, hence Riemann integrable and nonnegative. Values chosen at the finitely many corners do not change its integral. For a singleton interval the empty sum is zero; a constant curve also has zero length. Partition independence is established next.