I am studying the eigenfunctions and eigenvalues of the Laplacian on an open, bounded domain $\Omega \subset \mathbb{R}^n$ with homogeneous Dirichlet boundary conditions. I have read about the the weak and variational formulation of the problem. I understand the result that the first eigenvalue is given by: $$ \lambda_1 = \inf_{H_0^1(\Omega)} R = \inf_{v \in H_0^1(\Omega)} \frac{\int_\Omega \| \nabla v\|^2 \, \mathrm{d}x}{\int_\Omega v^2 \, \mathrm{d}x}$$ and the associated eigenfunction is $u_1$ such that $R(u_1) = \lambda_1$, as well as the characterization of the nth eigenvalue/eigenfunction. I have proved some of the basic results, such as the fact that the sequence of eigenvalues is unbounded and eigenfunctions associated to different eigenvalues are orthogonal (both in $L^2(\Omega)$ and $H_0^1(\Omega)$).
Now I am trying to prove that the eigenfunctions $u_1,u_2,\ldots$ form a basis of $L^2(\Omega)$. I have seen some proofs of this fact (e.g. Jost's book on PDEs and Mihai Nica's article), but I am trying to use a different approach. I have a sketch of this proof but I need to fill in some details.
The proof argues by contradiction. We define $V$ to be the closure in $H_0^1(\Omega)$ of the set: $$\left\{ u \in H_0^1(\Omega) : \exists \, N \in \mathbb{N}: u = \sum_{n=1}^N\alpha_nu_n\right\},$$ where $\alpha_n \in \mathbb{R}$ and the $u_n$'s are the eigenfunctions. Then $V$ is a closed subspace of $H_0^1(\Omega)$. We assume, for the sake of contradiction, that $V \neq H_0^1(\Omega)$.
1) This should then imply that $V^\perp \neq \{0\}$, but I am not sure why. I know that it is not necessary for a subset of a Hilbert space $H$ to be equal to the whole space $H$ for its orthogonal complement to be trivial. However here the space is closed so it is possible that this may force the orthogonal complement to be trivial, but I am not sure if that is enough.
Then $V^\perp$ is a non-trivial closed subspace of $H_0^1(\Omega)$ and hence we can apply the same methods used to determine the existence of eigenvalues and eigenfunctions to deduce the existence of an eigenfunction $u$ in $V^\perp$. It can then be shown that the eigenvalue associated to this eigenfunction must equal one of the previously determined eigenvalues (I understand how to do this).
2) Then I am not sure why this leads us to a contradiction. My guess is that then this $u\in V^\perp$ should equal some $u_n \in V$ (it is obvious that $V$ contains all the $u_n$'s) and this would imply that $V\cap V^\perp \neq \varnothing$, which is impossible.
3) This would then prove that $V = H_0^1(\Omega)$ but I have some doubts/confusion as to why this shows that the $u_n$'s form a basis of $H_0^1(\Omega)$, if they do.
4) Then I am not sure how to extend this to $L^2(\Omega)$. I suspect that the fact that $H_0^1(\Omega)$ is dense in $L^2(\Omega)$ should play a role.
I would be very grateful for any help (and/or references) on the numbered points.
This post was too long for a comment, so I write it here and I hope it will be useful.
$1)$ You can write $H^1_0(\Omega)=V\oplus V^{\perp}$ because $V$ is closed (it is a general fact for closed sets in Hilbert spaces), so $V=H^1_0(\Omega)$ iff $V^\perp=\{0\}$.
$2)$ Now if $u=u_n$, then $u\in V\cap V^\perp=\{0\}$, but $u_n\neq0$ because it is an eigenvector.
$3)$ Next, ${u_n}$ is an orthogonal basis of $H^1_0(\Omega)$ if $u_m\perp u_n$ when $m\neq n$ and if for all $u\in H^1_0(\Omega)$, $u=\sum \alpha_n u_n$ (strong limit).
$4)$ Finally, every $v\in L^2(\Omega)$ is a (strong) limit of elements $v_n$ is $H^1_0(\Omega)$ (by density), hence : $$\forall\varepsilon>0,\exists N\in\mathbb{N};\forall n\geq N,\|v-v_n\|<\varepsilon.$$ Write $v_n=\sum_k\alpha_{k,n}u_{k,n}$ with $\alpha_{k,n}$ some real numbers and $u_{k,n}$ some eigenvectors to conclude.