[proofplan] We first prove Bessel's finite-dimensional identity for the [orthogonal projection](/theorems/437) of a vector onto the span of finitely many basis vectors. This identity shows that the coordinate family of each $x \in H$ lies in $\ell^2(I)$ and that the finite coordinate sums form a Cauchy net. Completeness of $H$ gives the synthesis map from $\ell^2(I)$ to $H$, and the density of the span of the [orthonormal basis](/page/Orthonormal%20Basis) identifies this synthesis map with the inverse of the coordinate map. The norm identities then prove that the map is an isometric isomorphism. [/proofplan]

[step:Compute the finite orthogonal projection identity]Let $F \subset I$ be finite. Define the finite coordinate projection map \begin{align*} P_F: H &\to H \\ x &\mapsto \sum_{i \in F} (x,e_i)_H e_i. \end{align*} For each $j \in F$, orthonormality gives \begin{align*} (x - P_F x,e_j)_H &= (x,e_j)_H - \sum_{i \in F} (x,e_i)_H (e_i,e_j)_H \\ &= (x,e_j)_H - (x,e_j)_H \\ &= 0. \end{align*} Thus $x - P_F x$ is orthogonal to $\operatorname{span}\{e_i : i \in F\}$, while $P_F x$ lies in that span. By the Pythagorean identity for orthogonal vectors in a [Hilbert space](/page/Hilbert%20Space), \begin{align*} \|x\|_H^2 &= \|P_F x\|_H^2 + \|x - P_F x\|_H^2. \end{align*} Using orthonormality again, \begin{align*} \|P_F x\|_H^2 &= \left\|\sum_{i \in F} (x,e_i)_H e_i\right\|_H^2 \\ &= \sum_{i \in F} |(x,e_i)_H|^2. \end{align*} Therefore \begin{align*} \sum_{i \in F} |(x,e_i)_H|^2 \leq \|x\|_H^2. \end{align*}[/step]

[guided]Fix a finite set $F \subset I$. Define the finite coordinate projection map \begin{align*} P_F: H &\to H \\ x &\mapsto \sum_{i \in F} (x,e_i)_H e_i. \end{align*} This is the natural finite projection onto the span of the basis vectors indexed by $F$. We verify the projection property directly. For $j \in F$, \begin{align*} (x - P_F x,e_j)_H &= (x,e_j)_H - \left(\sum_{i \in F} (x,e_i)_H e_i,e_j\right)_H \\ &= (x,e_j)_H - \sum_{i \in F} (x,e_i)_H (e_i,e_j)_H. \end{align*} Since the family $(e_i)_{i \in I}$ is orthonormal, $(e_i,e_j)_H = 0$ when $i \neq j$ and $(e_j,e_j)_H = 1$. Hence the sum collapses to the single term $(x,e_j)_H$, so \begin{align*} (x - P_F x,e_j)_H = 0. \end{align*} Thus $x - P_F x$ is orthogonal to every vector in $\operatorname{span}\{e_i : i \in F\}$, while $P_F x$ belongs to that span. Therefore $x - P_F x$ and $P_F x$ are orthogonal. The Pythagorean identity in a Hilbert space gives \begin{align*} \|x\|_H^2 &= \|P_F x\|_H^2 + \|x - P_F x\|_H^2. \end{align*} We now compute the norm of $P_F x$ using orthonormality: \begin{align*} \|P_F x\|_H^2 &= \left(\sum_{i \in F} (x,e_i)_H e_i,\sum_{j \in F} (x,e_j)_H e_j\right)_H \\ &= \sum_{i,j \in F} (x,e_i)_H \overline{(x,e_j)_H} (e_i,e_j)_H \\ &= \sum_{i \in F} |(x,e_i)_H|^2. \end{align*} Combining the two identities yields \begin{align*} \sum_{i \in F} |(x,e_i)_H|^2 \leq \|x\|_H^2. \end{align*} This is Bessel's finite estimate, and it is the key bound that makes the coordinate map land in $\ell^2(I)$.[/guided]

[step:Show the coordinate map is well-defined and linear] For $x \in H$, define the scalar family $Ux = ((x,e_i)_H)_{i \in I}$. The estimate from the previous step gives \begin{align*} \sup\left\{\sum_{i \in F} |(x,e_i)_H|^2 : F \subset I \text{ finite}\right\} \leq \|x\|_H^2. \end{align*} Hence $Ux \in \ell^2(I)$. Let $\alpha,\beta$ be scalars and let $x,y \in H$. For every $i \in I$, linearity of the [inner product](/page/Inner%20Product) in the first variable gives \begin{align*} (U(\alpha x+\beta y))_i &= (\alpha x+\beta y,e_i)_H \\ &= \alpha(x,e_i)_H+\beta(y,e_i)_H \\ &= (\alpha Ux+\beta Uy)_i. \end{align*} Therefore $U:H \to \ell^2(I)$ is linear. [/step]

[step:Construct the synthesis map by finite partial sums]Let $a = (a_i)_{i \in I} \in \ell^2(I)$. For every finite subset $F \subset I$, define the finite synthesis map \begin{align*} S_F: \ell^2(I) &\to H \\ a &\mapsto \sum_{i \in F} a_i e_i. \end{align*} We claim that the net $(S_F(a))_F$, indexed by finite subsets of $I$ ordered by inclusion, is Cauchy in $H$. Set \begin{align*} M := \|a\|_{\ell^2(I)}^2 = \sup\left\{\sum_{i \in F} |a_i|^2 : F \subset I \text{ finite}\right\}. \end{align*} Let $\varepsilon > 0$. By the definition of supremum, there is a finite subset $F_0 \subset I$ such that \begin{align*} M - \varepsilon^2 < \sum_{i \in F_0} |a_i|^2 \leq M. \end{align*} If $E \subset I \setminus F_0$ is finite, then \begin{align*} \sum_{i \in E} |a_i|^2 &= \sum_{i \in F_0 \cup E} |a_i|^2 - \sum_{i \in F_0} |a_i|^2 \\ &\leq M - \sum_{i \in F_0} |a_i|^2 \\ &< \varepsilon^2. \end{align*} Now take finite subsets $F,G \subset I$ with $F_0 \subset F$ and $F_0 \subset G$. Since the vectors $e_i$ are orthonormal, \begin{align*} \|S_F(a)-S_G(a)\|_H^2 &= \left\|\sum_{i \in F \setminus G} a_i e_i - \sum_{i \in G \setminus F} a_i e_i\right\|_H^2 \\ &= \sum_{i \in F \triangle G} |a_i|^2 \\ &< \varepsilon^2, \end{align*} because $F \triangle G \subset I \setminus F_0$ is finite. Hence $(S_F(a))_F$ is Cauchy. Since $H$ is complete, this net converges in $H$. Define \begin{align*} V: \ell^2(I) &\to H \\ a &\mapsto \lim_F S_F(a). \end{align*}[/step]

[guided]We now build the inverse candidate. Given a square-summable family $a = (a_i)_{i \in I}$, the intended vector is the possibly infinite sum $\sum_{i \in I} a_i e_i$. Since $I$ may be uncountable, this sum must be interpreted as a net over finite subsets. For each finite $F \subset I$, define the finite synthesis map \begin{align*} S_F: \ell^2(I) &\to H \\ a &\mapsto \sum_{i \in F} a_i e_i. \end{align*} The finite subsets of $I$ are directed by inclusion: given finite $F$ and $G$, the finite set $F \cup G$ contains both. Thus $(S_F(a))_F$ is a well-defined net in $H$. We prove this net is Cauchy. Let \begin{align*} M := \|a\|_{\ell^2(I)}^2 = \sup\left\{\sum_{i \in F} |a_i|^2 : F \subset I \text{ finite}\right\}. \end{align*} The number $M$ is finite because $a \in \ell^2(I)$. Fix $\varepsilon > 0$. By the definition of the supremum, choose a finite set $F_0 \subset I$ such that \begin{align*} M - \varepsilon^2 < \sum_{i \in F_0} |a_i|^2 \leq M. \end{align*} This choice says that $F_0$ captures all but less than $\varepsilon^2$ of the finite square mass. Indeed, if $E \subset I \setminus F_0$ is finite, then $F_0 \cup E$ is finite, so \begin{align*} \sum_{i \in F_0 \cup E} |a_i|^2 \leq M. \end{align*} Since $F_0$ and $E$ are disjoint, \begin{align*} \sum_{i \in E} |a_i|^2 &= \sum_{i \in F_0 \cup E} |a_i|^2 - \sum_{i \in F_0} |a_i|^2 \\ &\leq M - \sum_{i \in F_0} |a_i|^2 \\ &< \varepsilon^2. \end{align*} Now take finite sets $F,G \subset I$ containing $F_0$. The difference of the corresponding partial sums only involves indices outside $F_0$: \begin{align*} S_F(a)-S_G(a) = \sum_{i \in F \setminus G} a_i e_i - \sum_{i \in G \setminus F} a_i e_i. \end{align*} The two families of basis vectors appearing here are orthonormal and indexed by the finite set $F \triangle G$. Therefore \begin{align*} \|S_F(a)-S_G(a)\|_H^2 &= \sum_{i \in F \triangle G} |a_i|^2. \end{align*} Since $F \triangle G \subset I \setminus F_0$, the tail estimate gives \begin{align*} \|S_F(a)-S_G(a)\|_H^2 < \varepsilon^2. \end{align*} Thus $(S_F(a))_F$ is Cauchy in the norm of $H$. Because $H$ is complete, this net converges. We define the synthesis map by \begin{align*} V: \ell^2(I) &\to H \\ a &\mapsto \lim_F \sum_{i \in F} a_i e_i. \end{align*}[/guided]

[step:Compute the coordinates and norm of the synthesized vector] Let $a = (a_i)_{i \in I} \in \ell^2(I)$, and let \begin{align*} Va = \lim_F S_F(a) \end{align*} in $H$. Fix $j \in I$. Since the map \begin{align*} \varphi_j: H &\to \mathbb{K} \\ x &\mapsto (x,e_j)_H \end{align*} is continuous, where $\mathbb{K}$ is the scalar field of $H$, we have \begin{align*} (Va,e_j)_H &= \lim_F (S_F(a),e_j)_H. \end{align*} For every finite $F \subset I$ with $j \in F$, \begin{align*} (S_F(a),e_j)_H &= \left(\sum_{i \in F} a_i e_i,e_j\right)_H \\ &= \sum_{i \in F} a_i(e_i,e_j)_H \\ &= a_j. \end{align*} Therefore $(Va,e_j)_H = a_j$ for every $j \in I$, so \begin{align*} UVa = a. \end{align*} Also, for each finite $F \subset I$, \begin{align*} \|S_F(a)\|_H^2 = \sum_{i \in F} |a_i|^2. \end{align*} The net \begin{align*} F \mapsto \sum_{i \in F} |a_i|^2 \end{align*} is increasing with respect to inclusion and bounded above by $\|a\|_{\ell^2(I)}^2$; by the definition of the supremum of these finite partial sums, it converges to \begin{align*} \sup\left\{\sum_{i \in F} |a_i|^2 : F \subset I \text{ finite}\right\}. \end{align*} Taking the limit along finite subsets and using norm continuity, \begin{align*} \|Va\|_H^2 &= \sup\left\{\sum_{i \in F} |a_i|^2 : F \subset I \text{ finite}\right\} \\ &= \|a\|_{\ell^2(I)}^2. \end{align*} Hence $V$ is an isometry from $\ell^2(I)$ into $H$. [/step]

[step:Use density of the orthonormal basis to identify the inverse on $H$]Let $x \in H$. The vector $VUx \in H$ satisfies, for every $j \in I$, \begin{align*} (VUx,e_j)_H = (Ux)_j = (x,e_j)_H. \end{align*} Define \begin{align*} w := x - VUx \in H. \end{align*} Then for every $j \in I$, \begin{align*} (w,e_j)_H = (x,e_j)_H - (VUx,e_j)_H = 0. \end{align*} Thus $w$ is orthogonal to every vector in $\operatorname{span}\{e_i : i \in I\}$. Since \begin{align*} \overline{\operatorname{span}\{e_i : i \in I\}} = H, \end{align*} continuity of the inner product implies that $w$ is orthogonal to every vector in $H$. Taking the inner product with $w$ itself gives \begin{align*} \|w\|_H^2 = (w,w)_H = 0. \end{align*} Therefore $w = 0$, so \begin{align*} VUx = x. \end{align*}[/step]

[guided]We already proved that $UVa = a$ for every $a \in \ell^2(I)$. To prove that $V$ is also a left inverse of $U$, fix $x \in H$. The vector $VUx$ is obtained by synthesizing the coordinate family of $x$: \begin{align*} VUx = \lim_F \sum_{i \in F} (x,e_i)_H e_i. \end{align*} Fix $j \in I$. Since $VUx$ is the norm limit of the finite sums $S_F(Ux)$ and the functional $y \mapsto (y,e_j)_H$ is continuous on $H$, we have \begin{align*} (VUx,e_j)_H = \lim_F (S_F(Ux),e_j)_H. \end{align*} For every finite $F \subset I$ with $j \in F$, orthonormality gives \begin{align*} (S_F(Ux),e_j)_H &= \left(\sum_{i \in F} (x,e_i)_H e_i,e_j\right)_H \\ &= \sum_{i \in F} (x,e_i)_H(e_i,e_j)_H \\ &= (x,e_j)_H. \end{align*} Because every sufficiently large finite subset in the directed set contains $j$, the net of scalars is eventually equal to $(x,e_j)_H$. Therefore \begin{align*} (VUx,e_j)_H = (Ux)_j = (x,e_j)_H. \end{align*} Define the error vector \begin{align*} w := x - VUx. \end{align*} Then each coordinate of $w$ along the orthonormal basis is zero: \begin{align*} (w,e_j)_H &= (x,e_j)_H - (VUx,e_j)_H \\ &= 0. \end{align*} Hence $w$ is orthogonal to every $e_j$, and therefore to every finite linear combination of the $e_j$. Now we use the basis hypothesis. The assumption that $(e_i)_{i \in I}$ is an orthonormal basis means \begin{align*} \overline{\operatorname{span}\{e_i : i \in I\}} = H. \end{align*} Since the map $y \mapsto (w,y)_H$ is continuous on $H$, orthogonality to the dense subspace $\operatorname{span}\{e_i : i \in I\}$ implies orthogonality to all of $H$. In particular, taking $y = w$ gives \begin{align*} 0 = (w,w)_H = \|w\|_H^2. \end{align*} Thus $w = 0$, and so \begin{align*} VUx = x. \end{align*} This proves that synthesis recovers every vector from its coordinates.[/guided]

[step:Conclude that the coordinate map is a linear isometric isomorphism] We have shown that $U:H \to \ell^2(I)$ is linear and that $V:\ell^2(I) \to H$ satisfies \begin{align*} UV = \operatorname{id}_{\ell^2(I)} \qquad\text{and}\qquad VU = \operatorname{id}_H. \end{align*} Therefore $U$ is bijective and $V = U^{-1}$. Finally, for $x \in H$, using $VUx = x$ and the norm identity for $V$ gives \begin{align*} \|Ux\|_{\ell^2(I)} = \|VUx\|_H = \|x\|_H. \end{align*} Thus $U$ is an isometry. Its inverse is exactly \begin{align*} (a_i)_{i \in I} \mapsto \lim_F \sum_{i \in F} a_i e_i, \end{align*} where $F$ ranges over finite subsets of $I$ ordered by inclusion. This is the claimed coordinate isomorphism. [/step]