Proof of Elementary Properties of an Orthonormal Family

Throughout we use the conditions of Complex Inner Product Space and the facts collected in Elementary Properties of a Complex Inner Product, together with the properties of finite sums in Properties of Finite Sums of Vectors and Properties of Finite Sums. By the definition of a tuple, an $n$-tuple in a set $X$ is a map from $[n]$ to $X$, so those finite sums apply to tuples without change.

Preliminaries. Since $e$ is orthonormal, each $e_{k}$ is a unit vector, so $\lVert e_{k}\rVert=1$ and therefore $\langle e_{k},e_{k}\rangle=\lVert e_{k}\rVert^{2}=1$ by the definition of the induced norm; and $\langle e_{j},e_{k}\rangle=0$ for $j\ne k$ by orthogonality. We also use $\overline{z}z=|z|^{2}$, which is claim 3 of Properties of Complex Conjugation and Modulus.

Claim 1. Fix $j\in[n]$. By the first identity of claim 6 of Properties of Finite Sums of Vectors,

The $n$-tuple in $\mathbb{C}$ whose $k$-th component is $c_{k}\langle e_{j},e_{k}\rangle$ takes the value $0$ at every $k\in[n]$ with $k\ne j$, and at $k=j$ it takes the value $c_{j}\cdot1=c_{j}$. By claim 7 of Properties of Finite Sums its finite sum equals $c_{j}$.

Claim 2. Put $x=\sum_{k=1}^{n}c_{k}e_{k}$. By the definition of the induced norm, $\lVert x\rVert^{2}=\langle x,x\rangle$. By the second identity of claim 6 of Properties of Finite Sums of Vectors and then claim 1,

The $n$-tuples in $\mathbb{C}$ with components $\overline{c_{k}}c_{k}$ and $|c_{k}|^{2}$ coincide, so their finite sums coincide, giving $\lVert x\rVert^{2}=\sum_{k=1}^{n}|c_{k}|^{2}$.

Claim 3. Suppose $c\in\mathbb{C}^{n}$ satisfies $\sum_{k=1}^{n}c_{k}e_{k}=0_{V}$. For $j\in[n]$, claim 1 gives $c_{j}=\langle e_{j},0_{V}\rangle$, which is $0$ by claim 3 of Elementary Properties of a Complex Inner Product. Hence $c_{j}=0$ for every $j\in[n]$, which is the requirement of Linearly Independent Finite Family.

Claim 4. First, $w+p=(u+(-p))+p=u+((-p)+p)=u+0_{V}=u$ by the associativity of vector addition, the additive inverse property, and the neutrality of $0_{V}$, all from Vector Space over a Field and Elementary Identities in a Vector Space.

Fix $j\in[n]$. By additivity in the second argument (condition 2 of Complex Inner Product Space), homogeneity in the second argument (condition 3 of the same definition) applied to $-p=(-1)p$, where $(-1)p=-p$ by Elementary Identities in a Vector Space, and claim 1 applied with $c_{k}=\langle e_{k},u\rangle$,

Next, by the second identity of claim 6 of Properties of Finite Sums of Vectors,

and every component of the summed tuple is $0$ by the previous paragraph, so the sum is $0$ by claim 7 of Properties of Finite Sums applied with distinguished index $1$. Thus $p$ and $w$ are orthogonal, and by claim 1 of Symmetry of Orthogonality and the Pythagorean Identity so are $w$ and $p$.

By claim 2 of Symmetry of Orthogonality and the Pythagorean Identity applied to $w$ and $p$, and then claim 2 above with $c_{k}=\langle e_{k},u\rangle$,

which is the stated identity after using commutativity of addition in $\mathbb{R}$.

Claim 5. Write $B=\sum_{k=1}^{n}|\langle e_{k},u\rangle|^{2}$. By condition 4 of Complex Inner Product Space, $\lVert w\rVert^{2}=\langle w,w\rangle$ is a real number with $0\le\lVert w\rVert^{2}$. Adding $B$ to both sides of this inequality, which is permitted by the first order axiom of Ordered Field, gives $B\le B+\lVert w\rVert^{2}$, and the right-hand side equals $\lVert u\rVert^{2}$ by claim 4.