Peter–Weyl theorem

All finite-dimensional unitary representations may be transported to some ${\mathbb{C}}^d$, so their equivalence classes form a set. By AC choose one representative of each irreducible class and an orthonormal basis in each. Schur orthogonality gives an orthonormal family $\mathcal{B}=\{\sqrt{d_{\pi }}{\pi }_{ij}\}$; write $U$ for its closed linear span. A matrix coefficient of any finite-dimensional continuous unitary representation lies in the algebraic span of $\mathcal{B}$: decompose into irreducibles by [L2] and change finite-dimensional bases. Duals of unitary irreducibles are again continuous unitary irreducibles: their matrices are the conjugates of the original unitary matrices, and a proper nonzero invariant dual subspace would have a proper nonzero invariant annihilator in the original space.

Two continuous functions equal Haar-almost everywhere are equal everywhere: a nonzero value of their continuous difference would give a nonempty open set where its modulus is bounded below by a positive number, contrary to [L5]. Thus a class with a continuous representative has a unique such representative.

Fix $n$ and a nonzero eigenvalue $\lambda$ of $T_{k_n}$. Its eigenspace $E$ is finite-dimensional and left-invariant by [L3], since real inversion-invariant $k_n$ is Hermitian. Every $f\in E$ has the continuous representative ${\lambda }^{-1}{T}_{k_n}f$ by [L4], uniquely by step 1.2. Consequently the restriction $\sigma (x)=L_x{\mathrm{\mid }}_E$ is a finite-dimensional continuous unitary representation by [L2], acting also on these continuous representatives. Let $\mathrm{\ell }:E\to \mathbb{C}$ be evaluation at $e$. For each $f\in E$, $f(x)=(L_{x^{-1}}f)(e)=\mathrm{\ell }(\sigma (x^{-1})f)=({\sigma }^{\ast }(x)\mathrm{\ell })(f)$. In dual bases this is a linear combination of the matrix entries of ${\sigma }^{\ast }(x)$, hence belongs to $U$ by step 1.1. Therefore $E\subseteq U$.

By [L3] and step 2.1, $\overline{\mathrm{ran}{T}_{k_n}}\subseteq U$ for every $n$ (also when the nonzero-eigenspace family is empty). For any $H\in L^2(G)$, the vectors $T_{k_n}H\in U$ converge to $H$ by [L4]. Closedness of $U$ gives $U=L^2(G)$. Thus $\mathcal{B}$ is a Hilbert basis, and [L5] gives its norm-convergent Fourier expansion.

For an irreducible $\rho$, let $V_j(\rho )=\mathrm{span}\{{\rho }_{ij}:1\le i\le d_{\rho }\}$, for $1\le j\le d_{\rho }$. These spaces, including those for distinct representatives, are mutually orthogonal by [L1]. Matrix multiplication gives $L_x{\rho }_{ij}={\sum }_k{\rho }_{ik}(x^{-1}){\rho }_{kj}$, so the map from the $i$th dual basis vector to $\sqrt{d_{\rho }}{\rho }_{ij}$ identifies $V_j(\rho )$ unitarily with ${\rho }^{\ast }$. Their Hilbert direct sum is all of $L^2(G)$ by step 3.1. To see that there are no further copies of a fixed irreducible $\pi$, orthogonal projection onto each such block commutes with $L_x$: both the block and its orthogonal complement are invariant under the unitary action. Its restriction to an irreducible subrepresentation of type $\pi$ is an intertwiner, and a nonzero such map to an irreducible block is an isomorphism, since its kernel and image are invariant. It is therefore zero unless ${\rho }^{\ast }\cong \pi$. Completeness of the block sum then places every copy of $\pi$ in the sum of these blocks. Duality permutes irreducible classes and ${\pi }^{\ast \ast }\cong \pi$, so the $\pi$-isotypic summand is precisely ${⨁}_{j=1}^{d_{\pi }}{V}_j({\pi }^{\ast })$, with multiplicity $d_{\pi }$. Here ${\pi }^{\ast }$ may be replaced by its chosen equivalent representative. The trivial representation supplies the constant function, including for the trivial group. AC covers the selections in step 1.1 and the Haar, spectral and Hilbert-space suppliers.