Proof of Gram-Schmidt Orthonormalisation in a Real Inner Product Space

We use Span of a Finite Family of Vectors, The Span of a Finite Family is the Smallest Subspace Containing It, the finite-sum rules of Properties of Finite Sums of Vectors, and write $S$ for the successor map of Natural Numbers. For a tuple $u\in E^{p}$ and $x\in E$, $x\in\operatorname{span}(u)$ means $x=\sum_{k=1}^{p}c_{k}u_{k}$ for some $c:[p]\to\mathbb{R}$.

Two preliminary facts. (i) For $p\in\mathbb{N}$, $u\in E^{S(p)}$ and $u'$ the restriction of $u$ to $[p]$: by the recursion and restriction rules, $\sum_{k=1}^{S(p)}c_{k}u_{k}=\sum_{k=1}^{p}c_{k}u'_{k}+c_{S(p)}u_{S(p)}$ for every $c:[S(p)]\to\mathbb{R}$. Hence $\operatorname{span}(u)=\{w+t\,u_{S(p)}:w\in\operatorname{span}(u'),\ t\in\mathbb{R}\}$; in particular $\operatorname{span}(u')\subseteq\operatorname{span}(u)$ (take $t=0$). (ii) For $u\in E^{1}$, $\operatorname{span}(u)=\{c\,u_{1}:c\in\mathbb{R}\}$ by the recursion rule; this is $\{0_{E}\}$ if $u_{1}=0_{E}$ (claim 4 of Elementary Identities in a Vector Space), while if $u_{1}\ne 0_{E}$ then $e_{1}=|u_{1}|^{-1}u_{1}$ satisfies $|e_{1}|=|u_{1}|^{-1}|u_{1}|=1$ by Elementary Identities in a Real Inner Product Space §homogeneity (as $|u_{1}|>0$ by Elementary Identities in a Real Inner Product Space §vanishing, so that $|u_{1}|^{-1}>0$ equals its absolute value by claim 1 of Properties of the Absolute Value in an Ordered Field) and $\operatorname{span}(e)=\{c\,e_{1}:c\in\mathbb{R}\}=\{c\,u_{1}:c\in\mathbb{R}\}=\operatorname{span}(u)$ for the $1$-tuple $e$ with component $e_{1}$, since $c\,u_{1}=(c|u_{1}|)e_{1}$ and $c\,e_{1}=(c|u_{1}|^{-1})u_{1}$; a $1$-tuple $e$ with $|e_{1}|=1$ is orthonormal by Orthogonality, Orthogonal Complement and Orthonormal Families in a Real Inner Product Space §orthonormal.

Claim 1. Let $A$ be the set of $n\in\mathbb{N}$ such that for every $v\in E^{n}$, either $\operatorname{span}(v)=\{0_{E}\}$ or there are $m\in\mathbb{N}$ with $m\le n$ and an orthonormal $e\in E^{m}$ with $\operatorname{span}(e)=\operatorname{span}(v)$. By (ii), $1\in A$. Let $n\in A$ and $v\in E^{S(n)}$; let $v'$ be the restriction of $v$ to $[n]$, $M'=\operatorname{span}(v')$, $M=\operatorname{span}(v)$ and $y=v_{S(n)}$, so that $M=\{w+ty:w\in M',t\in\mathbb{R}\}$ by (i).

Case $M'=\{0_{E}\}$. Then $M=\{ty:t\in\mathbb{R}\}$, which is $\{0_{E}\}$ if $y=0_{E}$; otherwise the $1$-tuple with component $|y|^{-1}y$ is orthonormal with span $M$ by (ii), and $1\le S(n)$ (claim 4 of Properties of the Order on the Natural Numbers).

Case $M'\ne\{0_{E}\}$. Since $n\in A$ there are $m'\le n$ and an orthonormal $e'\in E^{m'}$ with $\operatorname{span}(e')=M'$. Let $P$ be the map of Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace for $e'$, and put $w=y-Py$; by Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace §projection, $Py\in M'$ and $w$ lies in the orthogonal complement of $M'$. If $w=0_{E}$, then $y=Py\in M'$, so $M\subseteq M'$ (as $M'$ is a linear subspace) and $M'\subseteq M$ by (i); thus $M=M'=\operatorname{span}(e')$ and $m'\le n\le S(n)$ by claims 5 and 1 of Properties of the Order on the Natural Numbers. If $w\ne 0_{E}$, define $e\in E^{S(m')}$ by $e_{k}=e'_{k}$ for $k\in[m']$ and $e_{S(m')}=|w|^{-1}w$. Then $e$ is orthonormal: for $k\in[m']$, $\langle e'_{k},e_{S(m')}\rangle=|w|^{-1}\langle e'_{k},w\rangle=0$ because $e'_{k}\in M'$ (claim 1 of The Span of a Finite Family is the Smallest Subspace Containing It) and $w\in M'^{\perp}$, using symmetry; $|e_{S(m')}|=1$ as in (ii); and the remaining conditions are those of $e'$. Its span is $M$: each $e_{k}$ lies in $M$ (for $k\le m'$, $e'_{k}\in M'\subseteq M$; and $w=y-Py\in M$ since $y\in M$ by claim 1 of The Span of a Finite Family is the Smallest Subspace Containing It and $Py\in M'\subseteq M$), so $\operatorname{span}(e)\subseteq M$ by claim 3 of The Span of a Finite Family is the Smallest Subspace Containing It; conversely $M'=\operatorname{span}(e')\subseteq\operatorname{span}(e)$ by (i), and $y=Py+w=Py+|w|\,e_{S(m')}\in\operatorname{span}(e)$, so every $w'+ty$ with $w'\in M'$ lies in the linear subspace $\operatorname{span}(e)$, that is, $M\subseteq\operatorname{span}(e)$. Finally $S(m')\le S(n)$ since $m'\le n$, by claim 6 of Properties of the Order on the Natural Numbers. Hence $S(n)\in A$, and $A=\mathbb{N}$ by Principle of Induction for the Natural Numbers.

For the basis assertion, let $e\in E^{m}$ be orthonormal with $\operatorname{span}(e)=M$. By claim 2 of The Span of a Finite Family is the Smallest Subspace Containing It, the tuple $e^{\ast}\in M^{m}$ with the same components spans the vector space $M$. It is linearly independent in $M$: a relation $\sum_{k=1}^{m}c_{k}e^{\ast}_{k}=0_{E}$ formed in $M$ is the same relation formed in $E$ by claim 2 of A Linear Subspace is a Vector Space and Inherits an Inner Product, so $c=0$ by Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §independent. Hence $e^{\ast}$ is a basis of $M$.

Claim 2. Since $L\ne\{0_{E}\}$ is finite-dimensional, Finite-Dimensional Vector Space provides $p\in\mathbb{N}$ and a basis $b\in L^{p}$ of $L$. Let $b'\in E^{p}$ have the same components. Then $\operatorname{span}(b')=L$: every element of $L$ is a combination $\sum c_{k}b_{k}$ formed in $L$, which equals the same combination formed in $E$ (claim 2 of A Linear Subspace is a Vector Space and Inherits an Inner Product), so $L\subseteq\operatorname{span}(b')$; and $\operatorname{span}(b')\subseteq L$ by claim 3 of The Span of a Finite Family is the Smallest Subspace Containing It as each $b_{k}\in L$. Apply claim 1 to $b'$: since $\operatorname{span}(b')=L\ne\{0_{E}\}$, there are $m$ and an orthonormal $e\in E^{m}$ with $\operatorname{span}(e)=L$, and $e^{\ast}$ is a basis of $L$ by the basis assertion of claim 1.