Proof of Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space

Sums of vectors obey Properties of Finite Sums of Vectors and sums of real numbers obey Properties of Finite Sums; we use the recursion and restriction rules (claim 1 of each), and write $S$ for the successor map of Natural Numbers. Inner product identities are those of Real Inner Product Space §inner-product and Elementary Identities in a Real Inner Product Space §bilinear.

Claim 1. Let $A$ be the set of $n\in\mathbb{N}$ such that for every $n$-tuple $v\in E^{n}$ and every $w\in E$ one has $\langle\sum_{k=1}^{n}v_{k},w\rangle=\sum_{k=1}^{n}\langle v_{k},w\rangle$. For $n=1$ both sides equal $\langle v_{1},w\rangle$ by the recursion rules, so $1\in A$. Let $n\in A$ and let $v\in E^{S(n)}$, $w\in E$. Let $v'$ be the restriction of $v$ to $[n]$. By the recursion rule and the restriction rule, $\sum_{k=1}^{S(n)}v_{k}=\sum_{k=1}^{n}v'_{k}+v_{S(n)}$, and likewise $\sum_{k=1}^{S(n)}\langle v_{k},w\rangle=\sum_{k=1}^{n}\langle v'_{k},w\rangle+\langle v_{S(n)},w\rangle$. Hence, by additivity in the first argument and $n\in A$ applied to $v'$,

So $S(n)\in A$, and $A=\mathbb{N}$ by Principle of Induction for the Natural Numbers. The identity in the second argument follows by symmetry (a) applied to both sides.

Claim 2. Apply claim 1 to the $n$-tuple with components $c_{k}v_{k}$ and use homogeneity (c): $\langle c_{k}v_{k},w\rangle=c_{k}\langle v_{k},w\rangle$. The second identity follows by symmetry.

Claim 3. By claim 2, $\langle\sum_{k=1}^{n}c_{k}v_{k},v_{j}\rangle=\sum_{k=1}^{n}c_{k}\langle v_{k},v_{j}\rangle$. By orthonormality, $\langle v_{k},v_{j}\rangle=0$ for $k\ne j$ and $\langle v_{j},v_{j}\rangle=|v_{j}|^{2}=1$, so the $n$-tuple with components $c_{k}\langle v_{k},v_{j}\rangle$ has all components $0$ except possibly the $j$-th, which is $c_{j}$; its sum is $c_{j}$ by claim 7 of Properties of Finite Sums.

Claim 4. Put $u=\sum_{k=1}^{n}c_{k}v_{k}$. By Real Inner Product Space §norm, claim 2 (first identity, with $w=u$) and claim 3 together with symmetry, $|u|^{2}=\langle u,u\rangle=\sum_{k=1}^{n}c_{k}\langle v_{k},u\rangle=\sum_{k=1}^{n}c_{k}\langle u,v_{k}\rangle=\sum_{k=1}^{n}c_{k}c_{k}$.

Claim 5. Let $c:[n]\to\mathbb{R}$ satisfy $\sum_{k=1}^{n}c_{k}v_{k}=0_{E}$, the zero vector. For every $j\in[n]$, claim 3 and Elementary Identities in a Real Inner Product Space §zero give $c_{j}=\langle 0_{E},v_{j}\rangle=0$. This is linear independence.