Proof of A Real Hilbert Space Containing an Orthonormal Sequence Is Not Finite-Dimensional

Each result cited is universally quantified over the data in its own statement. For $s\in\mathbb{R}$ we write $s^{2}=ss$, and $|s|$ is the absolute value of $s$.

Suppose, for a contradiction, that $H$ is finite-dimensional.

Step 1 (the space is not the zero space). Since $(f_{j})_{j\in\mathbb{N}}$ is orthonormal, $\langle f_{1},f_{1}\rangle=1$ by Orthogonality, Orthogonal Complement and Orthonormal Families in a Real Inner Product Space (iii), that is, $|f_{1}|^{2}=1$ by Real Inner Product Spaces (ii). Were $f_{1}=0_{H}$, we should have $|f_{1}|=0$ by Elementary Identities in a Real Inner Product Space (iii) and hence $|f_{1}|^{2}=0$, whereas $0\ne1$ by claim 6 of Elementary Order Arithmetic in an Ordered Field. So $f_{1}\ne0_{H}$, and therefore $H\ne\{0_{H}\}$.

Step 2 (a spanning orthonormal tuple). The set $H$ is a linear subspace of $H$: it contains $0_{H}$ and is closed under the addition and scalar multiplication of $H$. It is finite-dimensional by assumption and differs from $\{0_{H}\}$ by step 1, so claim 2 of Gram-Schmidt Orthonormalisation in a Real Inner Product Space, applied with the inner product space $H$ in the role of $E$ and with $L=H$, provides a natural number $m$ and an orthonormal $m$-tuple $e\in H^{m}$, with components $e_{1},\dots,e_{m}$, such that $\operatorname{span}(e)=H$.

Step 3 (each member of the sequence has unit coordinate sum). Let $P:H\to H$ be the map of Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace formed with this $e$, namely $Px=\sum_{i=1}^{m}\langle x,e_{i}\rangle e_{i}$, and let $M=\operatorname{span}(e)$, so that $M=H$ by step 2. By Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace (i) we have $Px=x$ for every $x\in M$, hence for every $x\in H$; and by Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace (ii), $|Px|^{2}=\sum_{i=1}^{m}\langle x,e_{i}\rangle^{2}$. Taking $x=f_{j}$ and using $|f_{j}|^{2}=\langle f_{j},f_{j}\rangle=1$, which holds by Orthogonality, Orthogonal Complement and Orthonormal Families in a Real Inner Product Space (iii) and Real Inner Product Spaces (ii),

$$\sum_{i=1}^{m}\langle f_{j},e_{i}\rangle^{2}=1\qquad\text{for every }j\in\mathbb{N}.$$

Step 4 (each coordinate tends to zero). Let $i$ be a natural number with $1\le i\le m$. By Orthonormal Expansions in a Real Hilbert Space (i), applied to the orthonormal sequence $(f_{j})_{j\in\mathbb{N}}$ and to the vector $e_{i}$, the series $\sum_{j=1}^{\infty}\langle e_{i},f_{j}\rangle^{2}$ converges; hence the sequence $(\langle e_{i},f_{j}\rangle^{2})_{j\in\mathbb{N}}$ converges to $0$ by claim 2 of Elementary Properties of Series of Real Numbers. Since $\langle f_{j},e_{i}\rangle=\langle e_{i},f_{j}\rangle$ by Real Inner Product Spaces (i), the sequence $(\langle f_{j},e_{i}\rangle^{2})_{j\in\mathbb{N}}$ converges to $0$ as well.

Step 5 (contradiction). Apply Finite Sums of Real Numbers: Nonnegativity, Domination by the Sum, and Limits (iii) with $N=m$ to the $m$ sequences of step 4, indexed by $i$: the sequence whose $j$-th term is $\sum_{i=1}^{m}\langle f_{j},e_{i}\rangle^{2}$ converges to $\sum_{i=1}^{m}0$, which is $0$ by claim 3 of Properties of Finite Sums applied with $\lambda=0$. By step 3 that sequence is constant with value $1$. Taking $\varepsilon=1$ in Limit of a Sequence of Real Numbers there is accordingly some index at which $|1-0|<1$; but $0\le1$ by claim 1 of Elementary Arithmetic in an Ordered Field, so $|1-0|=|1|=1$ by claim 1 of Properties of the Absolute Value in an Ordered Field, and $1<1$ contradicts the irreflexivity of the strict order of Ordered Field.

Hence the assumption was false, and $H$ is not finite-dimensional.