Orthogonal Real Matrices

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$, with the set $\mathcal{M}_{n}(\mathbb{R})$ of square real matrices, the transpose $Q^{\top}$, the matrix product and the identity matrix $I_{n}$.

¶ A matrix $Q\in\mathcal{M}_{n}(\mathbb{R})$ is orthogonal if $Q^{\top}Q=I_{n}$.

¶ The set of orthogonal $n\times n$ matrices is

$$\mathrm{O}(n)=\{Q\in\mathcal{M}_{n}(\mathbb{R}):Q^{\top}Q=I_{n}\},$$

a subset of $\mathcal{M}_{n}(\mathbb{R})$.

¶ For $Q\in\mathcal{M}_{n}(\mathbb{R})$: $Q\in\mathrm{O}(n)$ if and only if $Q$ is orthogonal, that is, $Q^{\top}Q=I_{n}$.