Proof of An Orthonormal Basis of the Ambient Space Contained in the Form Space of a Hilbert Triple

Each result cited is universally quantified over the data in its own statement. Closures are taken in the topology of the metric indicated, and $\operatorname{cl}_{H}$ denotes the closure in $(H,d_{H})$, $\operatorname{cl}_{V}$ that in $(V,d_{V})$. Sums of vectors are finite sums in $H$, and $\operatorname{span}$ is the span of a tuple, a linear subspace of $H$ by claim 1 of The Span of a Finite Family is the Smallest Subspace Containing It and the smallest one containing the components of the tuple by claim 3 of that lemma.

Step 1 (a countable subset of $V$ dense in $H$). By Hilbert Triples: Standing Notation and Background §separable the metric space $(V,d_{V})$ is separable, so there is a countable subset $S\subseteq V$ with $\operatorname{cl}_{V}(S)=V$, that is, $S$ dense in $(V,d_{V})$.

We show that for every $x\in H$ and every positive $\varepsilon\in\mathbb{R}$ there is $s\in S$ with $|x-s|_{H}<\varepsilon$. Let $x$ and $\varepsilon$ be given. By Hilbert Triples: Standing Notation and Background §triple the subspace $V$ is dense in $H$, so $x\in H=\operatorname{cl}_{H}(V)$, and claim 3 of Characterization of the Closure in a Metric Space by Open Balls, applied in the metric space $(H,d_{H})$ to the subset $V$ and the point $x$, yields $y\in V$ with $|x-y|_{H}<\tfrac{\varepsilon}{2}$. Since $y\in V=\operatorname{cl}_{V}(S)$, the same claim of that theorem, applied in the metric space $(V,d_{V})$ to the subset $S$ and the point $y$, yields $s\in S$ with $|y-s|_{V}<\tfrac{\varepsilon}{2}$; and $|y-s|_{H}\le|y-s|_{V}$ by Hilbert Triples: Standing Notation and Background §triple, because $y-s\in V$. Hence, since $x-s=(x-y)+(y-s)$, The Norm Metric of a Real Inner Product Space: Triangle Inequalities, Limits and Continuity §triangle gives

Applying claim 3 of Characterization of the Closure in a Metric Space by Open Balls in the other direction, in $(H,d_{H})$ to the subset $S$, we conclude that every $x\in H$ lies in $\operatorname{cl}_{H}(S)$; since $\operatorname{cl}_{H}(S)\subseteq H$, this gives $\operatorname{cl}_{H}(S)=H$, so $S$ is dense in $H$.

Step 2 (an enumeration of $S$). Taking $x=0_{H}$ and $\varepsilon=1$ in Step 1 produces an element of $S$, so $S$ is nonempty. By Countable Set there is therefore a sequence $(s_{j})_{j\in\mathbb{N}}$ in $S$ whose set of terms is $S$; in particular $s_{j}\in V$ for every $j\in\mathbb{N}$, and every element of $S$ is a term of the sequence.

Step 3 (extending an orthonormal tuple inside $V$). We record the step used repeatedly below. Let $n\in\mathbb{N}$, let $f\in H^{n}$ be an orthonormal $n$-tuple all of whose components lie in $V$, let $M=\operatorname{span}(f)$, and let $P:H\to H$ be the map with $Px=\sum_{i=1}^{n}\langle x,f_{i}\rangle_{H}f_{i}$ of Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace, which applies because $H$ is a real inner product space. Let $z\in V$ with $z\notin M$. Since $V$ is a linear subspace of $H$ containing $f_{1},\dots,f_{n}$, the smallest such subspace satisfies $M\subseteq V$. By Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace §projection we have $Pz\in M$ and $z-Pz\in M^{\perp}$, the orthogonal complement of $M$. Put $w=z-Pz$. Then $w\in V$, because $z\in V$ and $Pz\in M\subseteq V$ and $V$ is a linear subspace; and $w\ne0_{H}$, since $w=0_{H}$ would give $z=Pz\in M$. Hence $0<|w|_{H}$ by Elementary Identities in a Real Inner Product Space §vanishing, and we may set $e=\tfrac{1}{|w|_{H}}w$, an element of $V$ with $|e|_{H}=\tfrac{1}{|w|_{H}}\,|w|_{H}=1$ by Elementary Identities in a Real Inner Product Space §homogeneity, the scalar $\tfrac{1}{|w|_{H}}$ being positive by claim 7 of Elementary Order Arithmetic in an Ordered Field. For $i\in[n]$ we have $\langle w,f_{i}\rangle_{H}=0$ because $w\in M^{\perp}$ and $f_{i}\in M$; hence, using the symmetry of the inner product in Real Inner Product Space §inner-product and the homogeneity in the second argument in Elementary Identities in a Real Inner Product Space §bilinear,

\langle x,s_{j}\rangle_{H}=\sum_{i=1}^{n}c_{i},\langle x,e_{i}\rangle_{H}=0

|x|{H},|x|{H}=\langle x,x\rangle_{H}=\langle x,x-s\rangle_{H}+\langle x,s\rangle_{H}=\langle x,x-s\rangle_{H}\le|x|{H},|x-s|{H}\le|x|_{H},\varepsilon .