I'm trying to solve an exercise in Brezis' Functional Analysis
Let $(H, \langle \cdot, \cdot \rangle)$ be a real Hilbert space and $|\cdot|$ its induced norm. Let $D$ be a subset of $H$ such that $\operatorname{span} D$ is dense in $H$. Let $(E_n)$ be a sequence of closed vector subspaces of $H$ that are mutually orthogonal, i.e., $\langle u, v \rangle =0$ for all $u\in E_m, v \in E_n$ with $m \neq n$. Assume that $$ \sum_{n=1}^\infty |\pi_{E_n} u|^2 = |u|^2 \quad \forall u \in D. $$ Here $\pi_{E_n} u$ is the orthogonal projection of $u$ onto $E_n$. Then $\operatorname{span} (\bigcup_{n=1}^\infty E_n)$ is dense in $H$.
Could you check if my attempt contains some logical mistakes?
Fix $u \in D$. Let $E := \overline{\operatorname{span} (\bigcup_{n=1}^\infty E_n)}$. We want to prove that $E = H$. It suffices to prove that $u \in E$ or equivalently $u = \pi_{E} u$. Let $u_n := \pi_{E_n} u$. Then $\sum_{n=1}^\infty u_n = \pi_{E} u$ and $\sum_{n=1}^\infty |u_n|^2 = |\pi_{E} u|^2$. Then $|u|^2 = |\pi_{E} u|^2$. By characterization of orthogonal projection, we have $$ |v-\pi_{E} u|^2 \le |v-u|^2- |\pi_{E} u-u|^2 \quad \forall v \in E. $$ With $v=0$, we get $|\pi_{E} u|^2 \le |u|^2- |\pi_{E} u-u|^2$. It follows that $|\pi_{E} u-u|^2=0$. This completes the proof.