Proof of Theorem OSLI

Let $S=\set{\vectorlist{u}{n}}$ be an orthogonal set of nonzero vectors. To prove the linear independence of $S$, we can appeal to the definition (Definition LICV) and begin with an arbitrary relation of linear dependence (Definition RLDCV), \begin{equation*} \lincombo{\alpha}{u}{n}=\zerovector. \end{equation*}

Then, for every $1\leq i\leq n$, we have \begin{align*} &\alpha_i\innerproduct{\vect{u}_i}{\vect{u}_i}\\ &\quad\quad=\alpha_1(0)+\alpha_2(0)+\cdots+\alpha_i\innerproduct{\vect{u}_i}{\vect{u}_i}+\cdots+\alpha_n(0) &&\knowl{./knowls/property.ZCN.knowl}{\text{Property ZCN}}\\ &\quad\quad= \alpha_1\innerproduct{\vect{u}_i}{\vect{u}_1}+ \cdots+ \alpha_i\innerproduct{\vect{u}_i}{\vect{u}_i}+ \cdots+ \alpha_n\innerproduct{\vect{u}_i}{\vect{u}_n} &&\knowl{./knowls/definition.OSV.knowl}{\text{Definition OSV}}\\ &\quad\quad= \innerproduct{\vect{u}_i}{\alpha_1\vect{u}_1}+ \innerproduct{\vect{u}_i}{\alpha_2\vect{u}_2}+ \cdots+ \innerproduct{\vect{u}_i}{\alpha_n\vect{u}_n} &&\knowl{./knowls/theorem.IPSM.knowl}{\text{Theorem IPSM}}\\ &\quad\quad= \innerproduct{\vect{u}_i}{\lincombo{\alpha}{u}{n}} &&\knowl{./knowls/theorem.IPVA.knowl}{\text{Theorem IPVA}}\\ &\quad\quad= \innerproduct{\vect{u}_i}{\zerovector} &&\knowl{./knowls/definition.RLDCV.knowl}{\text{Definition RLDCV}}\\ &\quad\quad=0 &&\knowl{./knowls/definition.IP.knowl}{\text{Definition IP}} \end{align*}

Because $\vect{u}_i$ was assumed to be nonzero, Theorem PIP says $\innerproduct{\vect{u}_i}{\vect{u}_i}$ is nonzero and thus $\alpha_i$ must be zero. So we conclude that $\alpha_i=0$ for all $1\leq i\leq n$ in any relation of linear dependence on $S$. But this says that $S$ is a linearly independent set since the only way to form a relation of linear dependence is the trivial way (Definition LICV). Boom!