Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$, let $Q,R\in\mathrm{O}(n)$, the set of orthogonal matrices, and let $x,y\in\mathbb{R}^{n}$, with the set $\mathcal{M}_{n}(\mathbb{R})$ of square real matrices and their entries, the transpose, the matrix product, the matrix-vector product, the identity matrix $I_{n}$ with entries $\delta_{ij}$, the standard basis vectors $e_{i}$, invertible matrices and their inverses $Q^{-1}$, the determinant $\det$, the components of points of $\mathbb{R}^{n}$ as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, their operations, sums of points of $\mathbb{R}^{n}$ formed in the commutative ring $\mathbb{R}^{[n]}$ of Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation §ring, the dot product, the Euclidean norm $\lVert\cdot\rVert$, and $[k]$ for $k\in\mathbb{N}_{0}$ as in Intervals of Natural Numbers §segment.

¶ $Q$ is invertible, $Q^{-1}=Q^{\top}$, $QQ^{\top}=I_{n}$ and $Q^{\top}\in\mathrm{O}(n)$.

¶ $I_{n}\in\mathrm{O}(n)$ and $QR\in\mathrm{O}(n)$.

¶ $(Qx)\cdot(Qy)=x\cdot y$ and $\lVert Qx\rVert=\lVert x\rVert$.

¶ A matrix $P\in\mathcal{M}_{n}(\mathbb{R})$ lies in $\mathrm{O}(n)$ if and only if $(Pe_{i})\cdot(Pe_{j})=\delta_{ij}$ for all $i,j\in[n]$.

¶ If $u:[n]\to\mathbb{R}^{n}$, $j\mapsto u_{j}$, satisfies $u_{i}\cdot u_{j}=\delta_{ij}$ for all $i,j\in[n]$, then the matrix $P\in\mathcal{M}_{n}(\mathbb{R})$ with entries $P_{ij}=(u_{j})_{i}$ ($i,j\in[n]$) lies in $\mathrm{O}(n)$, and $Pe_{j}=u_{j}$ for every $j\in[n]$.

¶ $\det Q\in\{1,-1\}$.

¶ If $k\in\mathbb{N}_{0}$, $k<n$, and $u:[k]\to\mathbb{R}^{n}$, $i\mapsto u_{i}$, is a map, then there is $v\in\mathbb{R}^{n}$ with $\lVert v\rVert=1$ and $v\cdot u_{i}=0$ for every $i\in[k]$. If moreover $u_{i}\cdot u_{j}=\delta_{ij}$ for all $i,j\in[k]$, then for every such $v$ the map $u':[k+1]\to\mathbb{R}^{n}$ with $u'_{i}=u_{i}$ ($i\in[k]$) and $u'_{k+1}=v$, which exists and is unique by Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §extension, satisfies $u'_{i}\cdot u'_{j}=\delta_{ij}$ for all $i,j\in[k+1]$; here $[k]\subseteq[k+1]\subseteq[n]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §inclusion, as $k<k+1\le n$.

¶ $x=\sum_{i=1}^{n}\bigl(x\cdot(Qe_{i})\bigr)\,Qe_{i}$.