Solution (source code)

= Solution

Using <orthogonality>,
$$
\|Qx\|^2=(Qx)^TQx=x^TQ^TQx=x^Tx=\|x\|^2.
$$
Both <norms> are nonnegative, so taking square <roots> proves
$$
\boxed{\|Qx\|=\|x\|.}
$$
Thus an <orthogonal matrix> is a <Euclidean isometry> fixing the origin.