The Standard Basis of the Complex Coordinate Space is an Orthonormal Basis

Let $n$ be a \reftext{def:natural-numbers-2026a}{natural number}, let $[n]$ be the \reftext{def:initial-segment-natural-numbers-2026a}{initial segment} determined by $n$, and let $\mathbb{C}^{n}$ be the \reftext{def:complex-coordinate-space-cn-2026a}{complex coordinate space}, which is a \reftext{def:vector-space-2026a}{complex vector space} by \ref{lem:cn-vector-space-2026a} and, together with the \reftext{def:standard-inner-product-cn-2026a}{standard inner product} $\langle\cdot,\cdot\rangle$, a \reftext{def:complex-inner-product-space-2026a}{complex inner product space} by claim 1 of \ref{lem:standard-inner-product-cn-2026a}. Let $\lVert\cdot\rVert$ be the \reftext{def:inner-product-norm-2026a}{induced norm}, let $e:[n]\to\mathbb{C}^{n}$ be the family of \reftext{def:standard-basis-cn-2026a}{standard basis vectors}, and let $u,v\in\mathbb{C}^{n}$ have components $u_{k}$ and $v_{k}$. Sums of vectors are \reftext{def:finite-sum-vector-space-2026a}{finite sums in $\mathbb{C}^{n}$} and sums of scalars are \reftext{def:finite-sum-field-2026b}{finite sums in a field}; $|z|$ is the \reftext{def:complex-modulus-2026a}{modulus} of a \reftext{def:complex-numbers-2026a}{complex number} $z$ and $\overline{z}$ its \reftext{def:complex-conjugate-2026a}{conjugate}. Then the following hold.

\textbf{1. (Components as coefficients)} For every $k\in[n]$,

\textbf{2. (Expansion)}

\textbf{3. (Orthonormal basis)} The family $e$ is an \reftext{def:orthonormal-basis-2026a}{orthonormal basis} of $\mathbb{C}^{n}$.

\textbf{4. (Parseval)}