[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.[/step]

[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: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]