Proving that the eigenfunctions of the Laplacian form a basis of $L^2(\Omega)$ (and of $H_0^1(\Omega)$)

I know a different approach, and I think it is more "standard." Basically it is sufficient to prove that if $\Omega \subset \mathbb{R}^n$ is limited open, then $(-\Delta)^{-1}$ is a compact and injective self-adjoint operator on $L^2(\Omega)$ and on $H^1_{0}(\Omega)$ and then after applies Hilbert-Schmidt spectral theorem. Recalling a little proof of the Hilbert-Schmidt spectral theorem, I think that what you ask lies precisely in the proof of this theorem. More precisely there is the following theorem

"If $H$ is a real (it is true also in the complex case) Hilbert spaces and $K:H \longrightarrow H$ is a compact adjoint operator, then exists an orthonormal basis of eigenvectors $\lbrace u_n \rbrace$ of $K$ with eigenvalues $\lbrace \lambda_n \rbrace$ and it has the representation

$\displaystyle Kx = \sum_{n \geq 1} \lambda_n (x, u_n)_H u_n$ $(x \in H)$"

Now, the facts you say apply generally to elliptic operators in divergence form, ie type

$\displaystyle Lu:= - \sum_{i,j=1}^n (a_{ij} u_{x_i})_{x_j} + \sum_{i=1}^n (b_i u)_{x_i} +c u$

where $a_{ij}, b_i, c \in L^\infty(\Omega)$, and it assumes that $L$ is uniformly elliptic. Basically the case of the Laplace operator is a particular case of $L$. After we introduce the weak solutions, assume $b_i=c=0$, there is the following theorem

"If $a_{ij}=a_{ji} \in L^\infty(\Omega)$, and considering $L^{-1} : L^2(\Omega) \longrightarrow H^1_{0}(\Omega) \subset L^2(\Omega)$, then $L^{-1}$ is a compact and injective self-adjoint operator. In addition there is an orthonormal basis $\lbrace \phi_k : k \in \mathbb{N} \rbrace$ of $L^2(\Omega)$ of eigenfunctions associated to the eigenvalues of $L^{-1}$ and

$\displaystyle L^{-1}f =\sum_{k=1}^\infty \lambda_k (f, \phi_k)_{L^2} \phi_k$

where $Lu=f$ wih $f \in L^2(\Omega)$. In particular $\lim_{k \rightarrow \infty} \lambda_k =0$".

This whole theory is very well explained in the book "Lecture Notes on Functional Analysis: With Applications to Linear Partial Differential Equations" by A. Bressan.