Matrix coefficients of finite-dimensional representations separate points of a compact group

By [F1] choose an open symmetric neighbourhood $U$ of $e$ with $g\mathrm{\notin }U\cdot U$ and by [F2] a continuous ${\phi }_0:K\to [0,1]$ with ${\phi }_0(e)=1$ and vanishing outside $U$; put $\phi (k):=\frac{1}{2}({\phi }_0(k)+{\phi }_0(k^{-1}))$, so $\phi \ge 0$ is continuous with $\phi (e)>0$, vanishing outside $U$ and $\phi (k^{-1})=\phi (k)$, hence ${\phi }^{\ast }=\phi$; put $\psi :=\phi \ast \phi \in C(K)$. Then $\psi$ is real and satisfies ${\psi }^{\ast }={\phi }^{\ast }\text{\hspace{0.17em}⁣}\ast {\phi }^{\ast }=\psi$ by [F3], and $\psi =C_{\phi }\phi$ because $C_{\phi }\phi (x)={\int }_K\phi (x{v}^{-1})\phi (v)d\mu (v)={\int }_K\phi (w)\phi (w^{-1}x)d\mu (w)=\psi (x)$ under the substitution $w=x{v}^{-1}$, which preserves $\mu$ by [F4]; moreover $\psi (e)={\int }_K\phi (v)\phi (v^{-1})d\mu (v)={\int }_K{\phi }^{2}d\mu >0$ because $\phi$ is continuous, positive at $e$ and $\mu$ is positive on the nonempty open set where $\phi >0$, while $\psi (g)={\int }_K\phi (v)\phi (v^{-1}g)d\mu (v)=0$ since $\phi (v)\phi (v^{-1}g)\mathrm{\ne }0$ would give $v\in U$ and $v^{-1}g\in U$, hence $g\in U\cdot U$ by symmetry of $U$; finally $C_{\phi }$ and $C_{\psi }$ are compact self-adjoint with the spectral decomposition $L^2(K)=\ker C_{\phi }\oplus {\widehat{⨁}}_{\lambda \mathrm{\ne }0}{E}_{\lambda }$ into finite-dimensional $\rho$-invariant pieces by [F5].

Suppose for contradiction that $\rho (g)$ acts as the identity on every nonzero eigenspace $E_{\lambda }$ of $C_{\phi }$. The spectral decomposition from step 1.1 and continuity of $\rho (g)$ imply that it is the identity on $(\ker C_{\phi }{)}^{\perp }$. Since $C_{\phi }$ is self-adjoint, its range is contained in that orthogonal complement: for $z\in \ker C_{\phi }$, $⟨C_{\phi }h,z⟩=⟨h,C_{\phi }z⟩=0$. Thus $\rho (g)C_{\phi }=C_{\phi }$, and applying this to $\phi$ gives $\rho (g)\psi =\psi$ in $L^2(K)$, where $\psi =C_{\phi }\phi$ from step 1.1. Both functions are continuous. Their almost-everywhere equality is therefore pointwise, since a nonzero continuous difference would be nonzero on a nonempty open set of positive Haar measure [F4]. At $e$ this gives $\psi (g)=\psi (e)$, contradicting $\psi (g)=0<\psi (e)$ from step 1.1. Hence some nonzero eigenspace of $C_{\phi }$ contains $\xi$ with $\rho (g)\xi \mathrm{\ne }\xi$.

For such $\lambda$ and $\xi$ put $\mathrm{\Pi }(k):=⟨\rho (k)\xi ,\rho (g)\xi -\xi ⟩$ and $u(k):=\mathrm{\Pi }(y^{-1}k)$; then $u(x)=\mathrm{\Pi }(g)=\mathrm{\parallel }\rho (g)\xi {\mathrm{\parallel }}^2-⟨\rho (g)\xi ,\xi ⟩$ and $u(y)=\mathrm{\Pi }(e)=⟨\xi ,\rho (g)\xi ⟩-\mathrm{\parallel }\xi {\mathrm{\parallel }}^2$, so $u(x)-u(y)=⟨\rho (g)\xi -\xi ,\rho (g)\xi -\xi ⟩=\mathrm{\parallel }\rho (g)\xi -\xi {\mathrm{\parallel }}^2>0$ and $u(x)\mathrm{\ne }u(y)$. On the other hand $u(k)=⟨\rho (k)\xi ,\rho (y)(\rho (g)\xi -\xi )⟩$ for every $k$, by unitarity of $\rho (y)$, so $u$ is a matrix coefficient of the finite-dimensional continuous unitary representation $\rho {\mathrm{\mid }}_{E_{\lambda }}$ with the vectors $\xi$ and $\rho (y)(\rho (g)\xi -\xi )$ [F8]; hence the finite-dimensional representations separate $x$ and $y$, which proves the lemma. Dependent Choice, and with it the Urysohn lemma used in [F2], is supplied by AC through [F9]; no other choice is made in the separation argument itself.