Mazur–Ulam theorem

Remarks

The heart of the proof is that $f$ preserves midpoints: $f\left(\frac{x + y}{2}\right) = \frac{f(x) + f(y)}{2}$. One proof describes the midpoint by distances only: it is fixed by every surjective isometry of $X$ that fixes $x$ and $y$. The argument uses the point reflection $z \mapsto x + y - z$, which swaps $x$ and $y$. Midpoint preservation and continuity then give real linearity of $f - f(0)$.

Surjectivity is needed. The map $f \colon \R \to \R^2$, $f(t) = (t, \sin t)$, with the norm $\norm{(a, b)} = \max(\abs{a}, \abs{b})$ on $\R^2$, is an isometry because $\abs{\sin t - \sin s} \le \abs{t - s}$, but it is not affine. The theorem is about real structure only: complex conjugation on $\C$ is a surjective isometry that is real-linear but not complex-linear.

Going deeper

For a student

The theorem shows that two real normed spaces are isometric as metric spaces exactly when they are isometrically isomorphic as normed spaces. So isometric classification of Banach spaces can ignore nonlinear isometries. For a Euclidean space it recovers the fact that every distance-preserving map of $\R^n$ onto itself is an orthogonal map followed by a translation.