The proof establishes the subgroup property, the inner-product preservation, and the determinant structure. **Step 1: $O_n(\mathbb{R})$ is a subgroup of $\mathrm{GL}_n(\mathbb{R})$.** First, $O_n(\mathbb{R}) \subseteq \mathrm{GL}_n(\mathbb{R})$: if $A^T A = I$, then $1 = \det(I) = \det(A^T)\det(A) = (\det A)^2$, so $\det A = \pm 1 \neq 0$. - *Identity:* $I_n^T I_n = I_n$, so $I_n \in O_n(\mathbb{R})$. - *Closure:* If $A^T A = I$ and $B^T B = I$, then $(AB)^T(AB) = B^T A^T A B = B^T B = I$. - *Inverses:* If $A^T A = I$, then $A^{-1} = A^T$, and $(A^T)^T A^T = A A^T = I$, so $A^{-1} \in O_n(\mathbb{R})$. **Step 2: Orthogonal matrices preserve the inner product.** For $A \in O_n(\mathbb{R})$ and $x, y \in \mathbb{R}^n$: \begin{align*} Ax \cdot Ay = (Ax)^T(Ay) = x^T A^T A y = x^T y = x \cdot y. \end{align*} Setting $x = y$ gives $|Ax| = |x|$, so $A$ is an isometry of $\mathbb{R}^n$. **Step 3: Determinant structure.** From Step 1, $\det A = \pm 1$ for all $A \in O_n(\mathbb{R})$. The restriction $\det : O_n(\mathbb{R}) \to (\{\pm 1\}, \times)$ is a surjective homomorphism (surjective because $I_n$ has determinant $+1$ and $\operatorname{diag}(-1, 1, \ldots, 1)$ has determinant $-1$). Its kernel is $\mathrm{SO}_n(\mathbb{R}) = \{A \in O_n(\mathbb{R}) : \det A = 1\}$, which is normal of index $2$ in $O_n(\mathbb{R})$. By the [First Isomorphism Theorem](/theorems/791): \begin{align*} O_n(\mathbb{R}) / \mathrm{SO}_n(\mathbb{R}) \cong C_2. \end{align*}