Proof of Orthonormal Expansion and Parseval's Identity in Finite Dimensions

Throughout, $[n]$ is the initial segment determined by $n$, and by the definition of a tuple an $n$-tuple in a set $X$ is a map from $[n]$ to $X$.

Claim 1. Suppose first that $e$ is an orthonormal basis of $V$. Then $e$ is a basis, so in particular it spans $V$. Let $u\in V$. By the spanning property there is $c\in\mathbb{C}^{n}$ with $u=\sum_{k=1}^{n}c_{k}e_{k}$. Applying claim 1 of Elementary Properties of an Orthonormal Family to this tuple gives, for every $j\in[n]$,

Thus $c$ coincides with the $n$-tuple in $\mathbb{C}$ whose $k$-th component is $\langle e_{k},u\rangle$, and therefore $u=\sum_{k=1}^{n}\langle e_{k},u\rangle e_{k}$.

Conversely, suppose that $u=\sum_{k=1}^{n}\langle e_{k},u\rangle e_{k}$ for every $u\in V$. Then for each $u\in V$ the $n$-tuple $c\in\mathbb{C}^{n}$ given by $c_{k}=\langle e_{k},u\rangle$ satisfies $u=\sum_{k=1}^{n}c_{k}e_{k}$, so $e$ spans $V$ in the sense of Finite Family Spanning a Vector Space. By claim 3 of Elementary Properties of an Orthonormal Family the tuple $e$ is linearly independent. Hence $e$ is a basis of $V$ by Finite Basis of a Vector Space, and since it is by hypothesis orthonormal, it is an orthonormal basis by Orthonormal Basis of a Complex Inner Product Space.

Claim 2. Assume $e$ is an orthonormal basis and let $u,w\in V$. By claim 1, $u=\sum_{k=1}^{n}\langle e_{k},u\rangle e_{k}$. Applying the second identity of claim 6 of Properties of Finite Sums of Vectors, with the scalars $c_{k}=\langle e_{k},u\rangle$ and the vectors $e_{k}$, gives

Taking $w=u$ yields

By claim 3 of Properties of Complex Conjugation and Modulus we have $\overline{z}z=|z|^{2}$ for every complex number $z$, so the $n$-tuples in $\mathbb{C}$ with components $\overline{\langle e_{k},u\rangle}\langle e_{k},u\rangle$ and $|\langle e_{k},u\rangle|^{2}$ coincide and hence have the same finite sum. Since $\lVert u\rVert^{2}=\langle u,u\rangle$ by the definition of the induced norm, this gives $\lVert u\rVert^{2}=\sum_{k=1}^{n}|\langle e_{k},u\rangle|^{2}$.