Proof of Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace

We use Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space, the finite-sum rules of Properties of Finite Sums of Vectors, and the identities of Elementary Identities in a Real Inner Product Space. Elements of $M=\operatorname{span}(e)$ are exactly the vectors $\sum_{i=1}^{m}c_{i}e_{i}$ with $c:[m]\to\mathbb{R}$ (Span of a Finite Family of Vectors).

Claim 1. For $x,x'\in E$ and $\lambda\in\mathbb{R}$, $\langle x+x',e_{i}\rangle=\langle x,e_{i}\rangle+\langle x',e_{i}\rangle$ and $\langle\lambda x,e_{i}\rangle=\lambda\langle x,e_{i}\rangle$ by conditions (b), (c) of Real Inner Product Space §inner-product, so the $m$-tuple with components $\langle x+x',e_{i}\rangle e_{i}$ is the componentwise sum of those for $x$ and $x'$, and the one for $\lambda x$ is $\lambda$ times the one for $x$ (using condition 8 and condition 5 of Vector Space over a Field); claims 2 and 3 of Properties of Finite Sums of Vectors give $P(x+x')=Px+Px'$ and $P(\lambda x)=\lambda Px$. Thus $P$ is linear. By its form, $Px\in M$. For $j\in[m]$, Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §coefficients with $c_{k}=\langle x,e_{k}\rangle$ gives $\langle Px,e_{j}\rangle=\langle x,e_{j}\rangle$, so $\langle x-Px,e_{j}\rangle=0$ by Elementary Identities in a Real Inner Product Space §bilinear. For $y=\sum_{j=1}^{m}c_{j}e_{j}\in M$, Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §combinations gives $\langle x-Px,y\rangle=\sum_{j=1}^{m}c_{j}\langle x-Px,e_{j}\rangle=0$ (all summands vanish, so the sum is its first summand $0$ by claim 7 of Properties of Finite Sums with $i=1$), so $x-Px\in M^{\perp}$. If $x\in M$, then $x-Px\in M$ (a linear subspace) and $x-Px\in M^{\perp}$, so $|x-Px|^{2}=\langle x-Px,x-Px\rangle=0$ and $x=Px$ by Elementary Identities in a Real Inner Product Space §vanishing.

Claim 2. $|Px|^{2}=\sum_{i=1}^{m}\langle x,e_{i}\rangle^{2}$ is Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §norm. Since $Px\in M$ and $x-Px\in M^{\perp}$, $\langle Px,x-Px\rangle=\langle x-Px,Px\rangle=0$, and Elementary Identities in a Real Inner Product Space §expansion applied to $x=Px+(x-Px)$ gives $|x|^{2}=|Px|^{2}+|x-Px|^{2}$. As squares are nonnegative, the translation rule (claim 3 of Elementary Arithmetic in an Ordered Field) gives $|Px|^{2}\le|x|^{2}$ and $|x-Px|^{2}\le|x|^{2}$, and claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field gives $|Px|\le|x|$ and $|x-Px|\le|x|$; the first inequality of the claim is the first of these with $|Px|^{2}$ expanded.

Claim 3. By linearity $Px-Py=P(x-y)$, so $|Px-Py|\le|x-y|$ by claim 2; that is, $d(Px,Py)\le 1\cdot d(x,y)$, and $1\ge 0$, which is the Lipschitz condition with constant $1$.

Claim 4. Let $(x_{k})$ be a sequence in $M$ converging to $x\in E$. For every $k$, using $Px_{k}=x_{k}$ (claim 1), The Norm Metric of a Real Inner Product Space: Triangle Inequalities, Limits and Continuity §triangle and claim 3, $|x-Px|\le|x-x_{k}|+|x_{k}-Px|=|x-x_{k}|+|Px_{k}-Px|\le 2|x-x_{k}|$. Given $\varepsilon>0$, choose $k$ with $|x-x_{k}|<\varepsilon/2$; then $|x-Px|<\varepsilon$. As $\varepsilon$ is arbitrary, $|x-Px|=0$ (if $|x-Px|>0$, take $\varepsilon=|x-Px|$), so $x=Px\in M$. Hence $M$ is closed by Sequential Characterization of Closed Subsets of a Metric Space.

Claim 5. Let $y\in M$. Then $Px-y\in M$ and $x-Px\in M^{\perp}$, so $\langle x-Px,Px-y\rangle=0$ and Elementary Identities in a Real Inner Product Space §expansion gives $|x-y|^{2}=|(x-Px)+(Px-y)|^{2}=|x-Px|^{2}+|Px-y|^{2}\ge|x-Px|^{2}$, whence $|x-Px|\le|x-y|$ by claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field. If $E$ is a real Hilbert space, then $M$ is a closed linear subspace by claim 4, and since $Px\in M$ and $x-Px\in M^{\perp}$, Orthogonal Projection onto a Closed Linear Subspace of a Real Hilbert Space §characterisation gives $Px=P_{M}x$.

Claim 6. Each coordinate $x\mapsto\langle x,e_{i}\rangle$ is linear by conditions (b), (c) of Real Inner Product Space §inner-product, and the vector operations of $\mathbb{R}^{m}$ are coordinatewise by Euclidean Space $\mathbb{R}^n$ is a Real Vector Space, so $\kappa$ is linear. Let $x\in M$; by claim 1, $x=Px=\sum_{i=1}^{m}\langle x,e_{i}\rangle e_{i}$. If $\kappa(x)$ has all coordinates $0$, then every summand is $0_{E}$ (claim 3 of Elementary Identities in a Vector Space) and $x=0_{E}$ by claim 7 of Properties of Finite Sums of Vectors; so $\kappa$ is injective (if $\kappa(x)=\kappa(y)$ then $\kappa(x-y)$ has all coordinates $0$). Given $\xi\in\mathbb{R}^{m}$, the vector $u=\sum_{i=1}^{m}\xi_{i}e_{i}$ lies in $M$ and $\langle u,e_{j}\rangle=\xi_{j}$ by Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §coefficients, so $\kappa(u)=\xi$; thus $\kappa$ is surjective with inverse $\xi\mapsto\sum_{i=1}^{m}\xi_{i}e_{i}$. For $x,y\in M$ put $\xi=\kappa(x)$, $\zeta=\kappa(y)$, so $x=\sum_{i}\xi_{i}e_{i}$ and $y=\sum_{j}\zeta_{j}e_{j}$. By Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §combinations and Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §coefficients (with symmetry), $\langle x,y\rangle=\sum_{i=1}^{m}\xi_{i}\langle e_{i},y\rangle=\sum_{i=1}^{m}\xi_{i}\zeta_{i}=\xi\cdot\zeta$ by Difference, Dot Product, and Orthogonality in $\mathbb{R}^n$. Finally $|x|^{2}=\sum_{i=1}^{m}\xi_{i}^{2}=\xi\cdot\xi=\lVert\xi\rVert^{2}$ by Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space §norm and claim 1 of Elementary Properties of the Euclidean Norm on $\mathbb{R}^n$; both $|x|$ and $\lVert\xi\rVert$ being nonnegative, $|x|=\lVert\xi\rVert$ by claim 3 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field.