Peter-Weyl decomposition of the regular representation

For a class $\pi$ of dimension $d_{\pi }$, the $d_{\pi }^2$ functions $c_{e_i,e_j}^{\pi }$ are linearly independent: if ${\sum }_{i,j}{\lambda }_{ij}{c}_{e_i,e_j}^{\pi }=0$, then by [F2] its squared $L^2$ norm is ${\sum }_{i,j}\mathrm{\mid }{\lambda }_{ij}{\mathrm{\mid }}^2\mathrm{/}{d}_{\pi }$, which must vanish, so every ${\lambda }_{ij}=0$; hence $M_{\pi }=\mathrm{span}\{c_{e_i,e_j}^{\pi }:i,j\}$ has dimension $d_{\pi }^2$, and because $u_{ij}^{\pi }=\sqrt{d_{\pi }}{c}_{e_i,e_j}^{\pi }$ it is also the span of the block $\{u_{ij}^{\pi }{\}}_{i,j}$; for inequivalent classes the coefficients are pairwise orthogonal by [F2], so $M_{\pi }\perp M_{\sigma }$. The closed span of ${\bigcup }_{\pi }{M}_{\pi }$ contains every $u_{ij}^{\pi }$ and hence the closed span of the Hilbert basis $\mathcal{B}$, which is $L^2(K)$ by [F1]; therefore $L^2(K)={\widehat{⨁}}_{\pi \in \widehat{K}}{M}_{\pi }$ is an orthogonal Hilbert-space direct sum of these blocks.

For all $g\in K$ and $v,w\in H_{\pi }$, [F3] gives $\rho (g)c_{v,w}^{\pi }(x)=c_{v,w}^{\pi }(xg)=⟨\pi (x)\pi (g)v,w⟩=c_{\pi (g)v,w}^{\pi }(x)$ and $\lambda (g)c_{v,w}^{\pi }(x)=c_{v,w}^{\pi }(g^{-1}x)=⟨\pi (g^{-1}x)v,w⟩=⟨\pi (x)v,\pi (g)w⟩=c_{v,\pi (g)w}^{\pi }(x)$, which are the stated action formulas. Fix the orthonormal basis $e_1,\dots ,e_d$ of $H_{\pi }$ and put $H_j:={\mathrm{span}}_i\{c_{e_i,e_j}^{\pi }\}$; each $H_j$ has dimension $d$ by the linear independence in step 1.1, satisfies $\rho (g)H_j\subseteq H_j$ by the first formula, and is the image of $H_{\pi }$ under the linear map $V_j(v):=c_{v,e_j}^{\pi }$ with $\rho (g)V_j=V_j\pi (g)$; since $\mathrm{\parallel }{c}_{v,e_j}^{\pi }{\mathrm{\parallel }}_2^2=d^{-1}\mathrm{\parallel }v{\mathrm{\parallel }}^2$ by [F2], $\sqrt{d}{V}_j$ is a unitary intertwiner $H_{\pi }\to H_j$. The sum ${\sum }_j{H}_j$ equals $M_{\pi }$ and ${\sum }_j\dim H_j=d^2=\dim M_{\pi }$, and [F2] makes distinct $H_j$ orthogonal, so $M_{\pi }={⨁}_{j=1}^d{H}_j$ is an orthogonal direct sum, and $\rho {\mathrm{\mid }}_{M_{\pi }}\cong d_{\pi }\pi$ by [F4].

On the same basis define the coordinate conjugation $J_{\pi }({\sum }_i{a}_i{e}_i)={\sum }_i\overline{a_i}{e}_i$ and $\bar{\pi }(g):=J_{\pi }\pi (g)J_{\pi }$; then $\bar{\pi }$ is a group homomorphism because $J_{\pi }^2=\mathrm{id}$, it is unitary because $J_{\pi }$ is a conjugate-linear isometry and $\pi (g)$ is unitary, it is strongly continuous because $J_{\pi }$ is isometric, and it satisfies $d_{\bar{\pi }}=d_{\pi }$ and $\overline{\stackrel{‾}{\pi }}=\pi$; moreover $\bar{\pi }$ is irreducible exactly when $\pi$ is, since $M\mapsto J_{\pi }M$ is a bijection between the closed invariant subspaces of $\bar{\pi }$ and those of $\pi$. The resulting class is independent of the choices: if $T:H_{\pi }\to H_{{\pi }^{\mathrm{\prime }}}$ is a unitary intertwiner and $J,J^{\mathrm{\prime }}$ are the two coordinate conjugations, then $J^{\mathrm{\prime }}TJ$ is a linear unitary intertwiner from $J\pi J$ to $J^{\mathrm{\prime }}{\pi }^{\mathrm{\prime }}{J}^{\mathrm{\prime }}$. Taking $T=I$ also covers a change of basis for the same representation. Conjugating twice returns the original class, so this defines a dimension-preserving involution of $\widehat{K}$. For the same basis define $G_i:={\mathrm{span}}_j\{c_{e_i,e_j}^{\pi }\}$; the second action formula of step 2.1 shows $\lambda (g)c_{e_i,e_j}^{\pi }=c_{e_i,\pi (g)e_j}^{\pi }={\sum }_l\overline{{\pi }_{lj}(g)}{c}_{e_i,e_l}^{\pi }$ with ${\pi }_{lj}(g)=⟨\pi (g)e_j,e_l⟩$, and $\overline{{\pi }_{lj}(g)}=⟨J_{\pi }\pi (g)e_j,e_l⟩=⟨\bar{\pi }(g)e_j,e_l⟩$ is exactly the $(l,j)$-entry of $\bar{\pi }(g)$; the linear map $W_i(e_j):=c_{e_i,e_j}^{\pi }$ therefore satisfies $\lambda (g)W_i=W_i\bar{\pi }(g)$ and $\sqrt{d}{W}_i$ is a unitary intertwiner $H_{\pi }\to G_i$ by [F2], while $M_{\pi }={⨁}_i{G}_i$ and $\dim G_i=d$ as in step 2.1; hence $\lambda {\mathrm{\mid }}_{M_{\pi }}\cong d_{\pi }\bar{\pi }$. Applying [F4] to the block decomposition of step 1.1 gives $\rho \cong {\widehat{⨁}}_{\pi }{d}_{\pi }\pi$ and $\lambda \cong {\widehat{⨁}}_{\pi }{d}_{\pi }\bar{\pi }$, and reindexing the latter sum by the involution $\pi \mapsto \bar{\pi }$ of $\widehat{K}$ gives $\lambda \cong {\widehat{⨁}}_{\pi }{d}_{\pi }\pi$, which completes the proof. The Axiom of Choice is inherited through the fixed representatives and bases and the cited suppliers.