[proofplan]
We use the defining matrix condition for the [orthogonal group](/page/Orthogonal%20Group), now included in the theorem statement: $A\in O(n)$ means $A^\top A=I_n$. The forward implication is a direct computation of the squared Euclidean norm. For the converse, preservation of norms implies preservation of squared norms, and expanding $|x+y|^2$ and $|x-y|^2$ recovers preservation of the Euclidean [inner product](/page/Inner%20Product). Evaluating the resulting bilinear identity on standard basis vectors gives $A^\top A=I_n$.
[/proofplan]
[step:Compute the squared norm from the orthogonality equation]
Let $\langle \cdot,\cdot\rangle:\mathbb{R}^n\times\mathbb{R}^n\to\mathbb{R}$ denote the standard Euclidean inner product, so that $\langle u,v\rangle=u^\top v$ and $|u|^2=\langle u,u\rangle$ for all $u,v\in\mathbb{R}^n$.
Assume $A\in O(n)$. By the definition of $O(n)$, this means
\begin{align*}
A^\top A=I_n.
\end{align*}
For any $x\in\mathbb{R}^n$, associativity of matrix multiplication gives
\begin{align*}
|Ax|^2=\langle Ax,Ax\rangle.
\end{align*}
Using the matrix representation of the Euclidean inner product,
\begin{align*}
\langle Ax,Ax\rangle=(Ax)^\top(Ax).
\end{align*}
Since $(Ax)^\top=x^\top A^\top$, we obtain
\begin{align*}
(Ax)^\top(Ax)=x^\top A^\top A x.
\end{align*}
Substituting $A^\top A=I_n$ gives
\begin{align*}
x^\top A^\top A x=x^\top I_n x.
\end{align*}
Finally,
\begin{align*}
x^\top I_n x=x^\top x=|x|^2.
\end{align*}
Thus $|Ax|^2=|x|^2$. Since both $|Ax|$ and $|x|$ are non-negative [real numbers](/page/Real%20Numbers), taking square roots gives $|Ax|=|x|$ for every $x\in\mathbb{R}^n$.
[/step]
[step:Recover all inner products from preservation of norms]
Assume conversely that $|Az|=|z|$ for every $z\in\mathbb{R}^n$. Squaring both sides gives
\begin{align*}
|Az|^2=|z|^2
\end{align*}
for every $z\in\mathbb{R}^n$.
Let $x,y\in\mathbb{R}^n$. We use the following polarization formula, verified here by expanding the two squared norms:
\begin{align*}
|x+y|^2-|x-y|^2=4\langle x,y\rangle.
\end{align*}
Applying this identity to the pair $Ax,Ay\in\mathbb{R}^n$ gives
\begin{align*}
4\langle Ax,Ay\rangle=|Ax+Ay|^2-|Ax-Ay|^2.
\end{align*}
By linearity of the matrix map $z\mapsto Az$, the right-hand side is
\begin{align*}
|A(x+y)|^2-|A(x-y)|^2.
\end{align*}
The norm-preservation hypothesis applied to $x+y$ and $x-y$ gives
\begin{align*}
|A(x+y)|^2-|A(x-y)|^2=|x+y|^2-|x-y|^2.
\end{align*}
Using the polarization identity again,
\begin{align*}
|x+y|^2-|x-y|^2=4\langle x,y\rangle.
\end{align*}
Therefore $4\langle Ax,Ay\rangle=4\langle x,y\rangle$, and division by $4$ gives
\begin{align*}
\langle Ax,Ay\rangle=\langle x,y\rangle.
\end{align*}
Since $x,y\in\mathbb{R}^n$ were arbitrary, $A$ preserves the Euclidean inner product.
[guided]
Assume that $|Az|=|z|$ for every vector $z\in\mathbb{R}^n$. We want to prove a stronger-looking statement: $A$ preserves not only lengths, but also angles, equivalently inner products. The tool that converts norm information into inner product information over $\mathbb{R}$ is the elementary expansion of $|x+y|^2$ and $|x-y|^2$.
First, squaring the hypothesis is valid because both sides are non-negative real numbers. Thus, for every $z\in\mathbb{R}^n$,
\begin{align*}
|Az|^2=|z|^2.
\end{align*}
Let $x,y\in\mathbb{R}^n$. The real polarization identity comes from expanding the two squared norms using bilinearity and symmetry of the Euclidean inner product:
\begin{align*}
|x+y|^2=\langle x+y,x+y\rangle=|x|^2+2\langle x,y\rangle+|y|^2.
\end{align*}
Similarly,
\begin{align*}
|x-y|^2=\langle x-y,x-y\rangle=|x|^2-2\langle x,y\rangle+|y|^2.
\end{align*}
Subtracting the second identity from the first gives
\begin{align*}
|x+y|^2-|x-y|^2=4\langle x,y\rangle.
\end{align*}
Now apply the same identity to the vectors $Ax$ and $Ay$. Since $A$ is a matrix, the map $z\mapsto Az$ is linear, so $Ax+Ay=A(x+y)$ and $Ax-Ay=A(x-y)$. Hence
\begin{align*}
4\langle Ax,Ay\rangle=|Ax+Ay|^2-|Ax-Ay|^2.
\end{align*}
Using linearity of $A$, this becomes
\begin{align*}
4\langle Ax,Ay\rangle=|A(x+y)|^2-|A(x-y)|^2.
\end{align*}
The hypothesis applies to every vector of $\mathbb{R}^n$, in particular to $x+y$ and $x-y$. Therefore
\begin{align*}
|A(x+y)|^2=|x+y|^2.
\end{align*}
Also,
\begin{align*}
|A(x-y)|^2=|x-y|^2.
\end{align*}
Substituting these two equalities gives
\begin{align*}
4\langle Ax,Ay\rangle=|x+y|^2-|x-y|^2.
\end{align*}
By the polarization identity already verified,
\begin{align*}
|x+y|^2-|x-y|^2=4\langle x,y\rangle.
\end{align*}
Thus
\begin{align*}
4\langle Ax,Ay\rangle=4\langle x,y\rangle.
\end{align*}
Dividing by $4$ gives
\begin{align*}
\langle Ax,Ay\rangle=\langle x,y\rangle.
\end{align*}
Because $x$ and $y$ were arbitrary vectors in $\mathbb{R}^n$, the matrix $A$ preserves the Euclidean inner product on all pairs of vectors.
[/guided]
[/step]
[step:Translate inner product preservation into the matrix equation $A^\top A=I_n$]
Let $B\in M_n(\mathbb{R})$ be the matrix
\begin{align*}
B:=A^\top A.
\end{align*}
From the previous step, for all $x,y\in\mathbb{R}^n$,
\begin{align*}
\langle Ax,Ay\rangle=\langle x,y\rangle.
\end{align*}
Using the matrix representation of the Euclidean inner product, this is
\begin{align*}
x^\top A^\top A y=x^\top y.
\end{align*}
Equivalently,
\begin{align*}
x^\top B y=x^\top I_n y
\end{align*}
for all $x,y\in\mathbb{R}^n$.
For each $i\in\{1,\dots,n\}$, let $e_i\in\mathbb{R}^n$ denote the $i$-th standard basis vector. Taking $x=e_i$ and $y=e_j$ gives
\begin{align*}
e_i^\top B e_j=e_i^\top I_n e_j
\end{align*}
for every $i,j\in\{1,\dots,n\}$. The left-hand side is the $(i,j)$-entry $B_{ij}$, and the right-hand side is the $(i,j)$-entry of $I_n$. Hence every entry of $B$ equals the corresponding entry of $I_n$, so
\begin{align*}
B=I_n.
\end{align*}
Since $B=A^\top A$, we have $A^\top A=I_n$. By the definition of $O(n)$, this means $A\in O(n)$. This proves the converse implication and completes the proof.
[/step]
