[proofplan]
We use the BGG resolution character identity for the finite-dimensional irreducible module $L(\lambda)$, expressed using the shifted Weyl [group action](/page/Group%20Action) $w\cdot\lambda=w(\lambda+\rho)-\rho$. Substituting the [Verma module character formula](/theorems/9383) turns the alternating sum of Verma characters into a single fraction with denominator $\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})$. The numerator is exactly $e^{-\rho}A_{\lambda+\rho}$, and the [Weyl denominator formula](/theorems/9382) identifies $A_\rho$ with $e^\rho\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})$.
[/proofplan]
[step:Set up the character ring and the shifted Weyl group action]
Let $\mathbb Z[P]$ denote the integral group algebra of the lattice $P$, with multiplication determined by
\begin{align*}
e^\mu e^\nu=e^{\mu+\nu}
\end{align*}
for $\mu,\nu\in P$. Since $P$ is a free abelian group of finite rank, $\mathbb Z[P]$ is a Laurent [polynomial ring](/page/Polynomial%20Ring) after choosing a basis of $P$, hence it is an [integral domain](/page/Integral%20Domain). Therefore its fraction field is well-defined.
For $w\in W$ and $\eta\in\mathfrak h^*$, define the shifted, or dot, action by
\begin{align*}
w\cdot\eta:=w(\eta+\rho)-\rho.
\end{align*}
Since $\rho(\alpha^\vee)=1$ for every simple root $\alpha$, we have $\rho\in P$. Hence $\lambda+\rho\in P$, and all terms $e^{w(\lambda+\rho)}$ occurring in $A_{\lambda+\rho}$ lie in $\mathbb Z[P]$.
[/step]
[step:Apply the BGG alternating character identity]
We use the following standard BGG character identity: for every dominant integral weight $\lambda\in P^+$, the finite-dimensional irreducible highest-weight module $L(\lambda)$ satisfies
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{w\in W}\det(w)\operatorname{ch}M(w\cdot\lambda)
\end{align*}
in the completed character algebra, where $M(\mu)$ denotes the Verma module of highest weight $\mu$. This is the character identity induced by the BGG resolution of $L(\lambda)$ by Verma modules. The hypothesis $\lambda\in P^+$ is precisely the dominant integral hypothesis under which the finite-dimensional irreducible module $L(\lambda)$ is the module resolved by this BGG complex; equivalently, this is the finite-dimensional highest-weight module appearing in the classification theorem [citetheorem:9373].
The sum is finite because $W$ is finite, so no convergence issue occurs in the alternating sum over $W$ itself.
[/step]
[step:Substitute the Verma module character formula]
For every $\mu\in\mathfrak h^*$, the Verma module character formula [citetheorem:9383] gives
\begin{align*}
\operatorname{ch}M(\mu)=\frac{e^\mu}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}
\end{align*}
as an identity in the usual completion of the group algebra determined by the positive root cone. Applying this with $\mu=w\cdot\lambda$ for each $w\in W$ gives
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{w\in W}\det(w)\frac{e^{w\cdot\lambda}}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
Since the denominator does not depend on $w$, the finite sum can be combined into one fraction:
\begin{align*}
\operatorname{ch}L(\lambda)=\frac{\sum_{w\in W}\det(w)e^{w\cdot\lambda}}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
[guided]
The BGG identity has reduced the character of $L(\lambda)$ to a finite alternating sum of Verma module characters. The next input is the Verma module character formula [citetheorem:9383], which says that a Verma module with highest weight $\mu$ has character
\begin{align*}
\operatorname{ch}M(\mu)=\frac{e^\mu}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
The formula applies here to every $\mu=w\cdot\lambda$ because $M(w\cdot\lambda)$ is a Verma module with highest weight $w\cdot\lambda$ by definition.
Substituting this formula into the BGG identity gives
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{w\in W}\det(w)\frac{e^{w\cdot\lambda}}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
The denominator is the same for every element $w\in W$, and the Weyl group $W$ is finite. Hence the alternating sum may be collected over the common denominator:
\begin{align*}
\operatorname{ch}L(\lambda)=\frac{\sum_{w\in W}\det(w)e^{w\cdot\lambda}}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
This is the point where the proof becomes a bookkeeping problem: we must rewrite the numerator using the definition of the dot action and then identify the denominator with the Weyl denominator.
[/guided]
[/step]
[step:Rewrite the alternating numerator as a Weyl alternant]
By the definition of the dot action,
\begin{align*}
w\cdot\lambda=w(\lambda+\rho)-\rho.
\end{align*}
Therefore
\begin{align*}
e^{w\cdot\lambda}=e^{w(\lambda+\rho)-\rho}=e^{-\rho}e^{w(\lambda+\rho)}.
\end{align*}
Substituting this into the numerator yields
\begin{align*}
\sum_{w\in W}\det(w)e^{w\cdot\lambda}=e^{-\rho}\sum_{w\in W}\det(w)e^{w(\lambda+\rho)}.
\end{align*}
By the definition of the Weyl alternant, the sum on the right is $A_{\lambda+\rho}$. Hence
\begin{align*}
\operatorname{ch}L(\lambda)=\frac{e^{-\rho}A_{\lambda+\rho}}{\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
Multiplying numerator and denominator by $e^\rho$ gives
\begin{align*}
\operatorname{ch}L(\lambda)=\frac{A_{\lambda+\rho}}{e^\rho\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})}.
\end{align*}
[/step]
[step:Use the Weyl denominator formula to identify the denominator]
The Weyl denominator formula [citetheorem:9382] states that
\begin{align*}
A_\rho=e^\rho\prod_{\alpha\in\Phi^+}(1-e^{-\alpha}).
\end{align*}
Substituting this identity into the previous expression gives
\begin{align*}
\operatorname{ch}L(\lambda)=\frac{A_{\lambda+\rho}}{A_\rho}.
\end{align*}
The denominator is nonzero because the Weyl denominator formula writes it as $e^\rho$ multiplied by the finite product of nonzero factors $1-e^{-\alpha}$ in the integral domain $\mathbb Z[P]$. Thus the quotient is meaningful in the fraction field of $\mathbb Z[P]$.
This proves both displayed formulas in the statement.
[/step]
