Orthogonality identifies the Weyl numerator

Pull the irreducible representation of highest character $\lambda$ to the cover. Surjectivity [L2] makes the pullback irreducible, since it has exactly the same invariant subspaces, and its character is the pullback of ${\chi }_{\lambda }$. Every central-factor operator commutes with the pulled-back representation; over $\mathbb{C}$ it has an eigenvalue, and its eigenspace is invariant, so irreducibility makes that operator scalar. If a subspace is invariant under the semisimple factor, it is therefore also invariant under the scalar central factor and hence under the whole product; thus the restriction to $G_{\mathrm{d}\mathrm{e}\mathrm{r}}^{sc}$ is irreducible. Applying the compact highest-weight classification in [L2] to that factor and the highest-weight bounds there, the torus expansion is a finite sum of weight characters with nonnegative integer multiplicities, ${\chi }_{\lambda }=e^{\lambda }+{\sum }_{\mu <\lambda }{m}_{\mu }{e}^{\mu },$ with top multiplicity one. This expansion is W-invariant: conjugation by a normalizer representative acts on the representation by an invertible matrix and does not change its trace, and character independence from [L1] gives equality also in the formal algebra.

For any nontrivial torus character $e^{\gamma }$, choose t with $e^{\gamma }(t)\mathrm{\ne }1$. Translation invariance [L4] gives $I:=\int e^{\gamma }=e^{\gamma }(t)I$, hence I=0. The trivial character has integral one. Thus ${\int }_{T_p}{e}^{\eta }\overline{e^{\zeta }}dt={\delta }_{\eta \zeta }$. Using the regular-orbit statements in [L1], finite expansion consequently gives ${\int }_{T_p}{A}_{\eta }\overline{A_{\zeta }}dt=\mathrm{\mid }W\mathrm{\mid }{\delta }_{\eta \zeta }$ for strictly dominant $\eta ,\zeta$: distinct representatives have disjoint orbits and the same representative has exactly the $\mathrm{\mid }W\mathrm{\mid }$ equal-index matches, each with sign squared one. This uses only finite orthogonality, not completeness of a Fourier basis.

Since $e^{\rho }$ is a circle character, it has modulus one. Taking the squared absolute value of the product identity [L1] and using [L4] proves pointwise on $T_p$ that $\mathrm{\mid }{A}_{\rho }{\mathrm{\mid }}^2=J$. This is valid also at zeros and for the empty product. After unitarizing the pulled-back irreducible without changing its trace, [L3] and Weyl integration on the cover applied to the continuous class function $\mathrm{\mid }{\chi }_{\lambda }{\mathrm{\mid }}^2$ give ${\int }_{T_p}\mathrm{\mid }{A}_{\rho }{\chi }_{\lambda }{\mathrm{\mid }}^{2}dt=\mathrm{\mid }W\mathrm{\mid }\mathrm{.}$

Put $F=A_{\rho }{\chi }_{\lambda }$. It is a finite anti-invariant integral sum by [L1] and step 1.1. Expand $A_{\rho }$ using its product expression. Every exponent of F is $\lambda +\rho -\sigma$ with $\sigma$ in the nonnegative simple-root cone; the coefficient at $\lambda +\rho$ is one, because achieving it requires both the top weight and the empty subset of positive roots. A nonzero sum in that cone cannot cancel another such sum. Since $\lambda$ is dominant and rho pairs to one with each simple coroot as in [L1], $\lambda +\rho$ is strictly dominant. In the orbit basis [L1] its coefficient is therefore one: that basis element contains $e^{\lambda +\rho }$ once, and no other indexed orbit contains it. Hence $F=A_{\lambda +\rho }+{\sum }_{\eta \mathrm{\ne }\lambda +\rho }{c}_{\eta }{A}_{\eta },$ a finite sum over strictly dominant characters $\eta$ with $c_{\eta }\in \mathbb{Z}$. No condition that $\eta -\rho$ be strictly dominant is imposed.

By step 1.2, the squared norm of the finite expansion in step 2.1 is $\mathrm{\mid }W\mathrm{\mid }(1+{\sum }_{\eta }\mathrm{\mid }{c}_{\eta }{\mathrm{\mid }}^2)$. Step 1.3 says the same squared norm is $\mathrm{\mid }W\mathrm{\mid }$. As $\mathrm{\mid }W\mathrm{\mid }>0$, every term $\mathrm{\mid }{c}_{\eta }{\mathrm{\mid }}^2$ is zero, proving $A_{\rho }{\chi }_{\lambda }=A_{\lambda +\rho }$ in the formal algebra and hence as functions. There is no infinite matrix, least element of a global dominance order, or induction to justify. When the roots are empty, W is trivial, rho=0 and the compact-group classification gives ${\chi }_{\lambda }=e^{\lambda }$, the same identity; for $\lambda =0$ it is $A_{\rho }=A_{\rho }$. Choice supplies the assumptions of the cited classification, cover and integration interfaces.