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

Let $\mathbb{R}$ be the ordered field of real numbers, with the notation of that item, let $E$ be a real inner product space with inner product $\langle\cdot,\cdot\rangle$, norm $|\cdot|$, let $n$ be a natural number with initial segment $[n]$, let $v\in E^{n}$ be an $n$-tuple in $E$ with components $v_{k}$, let $c:[n]\to\mathbb{R}$ be a map with values $c_{k}$, and let $w\in E$. Sums of vectors are finite sums in $E$, sums of real numbers are finite sums in the field $\mathbb{R}$, $\sum_{k=1}^{n}c_{k}v_{k}$ denotes the finite sum in $E$ of the $n$-tuple with components $c_{k}v_{k}$, and $\sum_{k=1}^{n}c_{k}^{2}$ the finite sum in $\mathbb{R}$ of the $n$-tuple with components $c_{k}^{2}=c_{k}c_{k}$. Then the following hold.

1. (Sums)(i) $\bigl\langle\sum_{k=1}^{n}v_{k},w\bigr\rangle=\sum_{k=1}^{n}\langle v_{k},w\rangle$ and $\bigl\langle w,\sum_{k=1}^{n}v_{k}\bigr\rangle=\sum_{k=1}^{n}\langle w,v_{k}\rangle$.

2. (Linear combinations)(ii) $\bigl\langle\sum_{k=1}^{n}c_{k}v_{k},w\bigr\rangle=\sum_{k=1}^{n}c_{k}\langle v_{k},w\rangle$ and $\bigl\langle w,\sum_{k=1}^{n}c_{k}v_{k}\bigr\rangle=\sum_{k=1}^{n}c_{k}\langle w,v_{k}\rangle$.

Suppose in addition that $v$ is orthonormal. Then the following hold.

3. (Coefficients)(iii) $\bigl\langle\sum_{k=1}^{n}c_{k}v_{k},v_{j}\bigr\rangle=c_{j}$ for every $j\in[n]$.

4. (Norm of a linear combination)(iv) $\bigl|\sum_{k=1}^{n}c_{k}v_{k}\bigr|^{2}=\sum_{k=1}^{n}c_{k}^{2}$.

5. (Linear independence)(v) The family $v$ is linearly independent.