[proofplan]
The proof is a synthesis of the highest-weight classification and the computational formulae proved for finite-dimensional modules. First we use the classification theorem to identify irreducible finite-dimensional modules with dominant integral highest weights. Then we invoke the Weyl character and dimension formulae, the dual-highest-weight theorem, and the character multiplication method for tensor products. The only structural input for the [tensor product](/page/Tensor%20Product) statement is complete reducibility, together with the uniqueness of expansion in irreducible characters.
[/proofplan]
[step:Identify finite-dimensional irreducible modules by dominant integral highest weights]
The hypotheses here are exactly those of [citetheorem:9373]: $\mathfrak g$ is a finite-dimensional complex semisimple [Lie algebra](/page/Lie%20Algebra), $\mathfrak h$ is a Cartan subalgebra, $\Phi^+$ is a chosen positive root system, and $P^+$ is the dominant integral cone determined by the corresponding simple roots. Therefore [citetheorem:9373] gives that for every $\lambda\in P^+$ there exists an irreducible finite-dimensional highest-weight module $L(\lambda)$ of highest weight $\lambda$, and that every irreducible finite-dimensional complex $\mathfrak g$-module is isomorphic to exactly one such $L(\lambda)$.
This proves the asserted bijection
\begin{align*}
P^+\longrightarrow \{\text{isomorphism classes of irreducible finite-dimensional }\mathfrak g\text{-modules}\}
\end{align*}
given by $\lambda\mapsto L(\lambda)$.
[guided]
The first part of the summary theorem is precisely the highest-weight classification. We check that its hypotheses match the present setting. The theorem [citetheorem:9373] applies to a finite-dimensional complex semisimple Lie algebra $\mathfrak g$, a Cartan subalgebra $\mathfrak h\subset\mathfrak g$, a root system $\Phi\subset\mathfrak h^*$, and a choice of positive roots $\Phi^+$. These are all part of the present theorem statement.
The same theorem states two facts at once. First, every dominant integral weight $\lambda\in P^+$ produces an irreducible finite-dimensional highest-weight module $L(\lambda)$. Second, if $V$ is any irreducible finite-dimensional complex $\mathfrak g$-module, then $V$ has a unique highest weight $\lambda\in P^+$ and is isomorphic to $L(\lambda)$. Thus the assignment
\begin{align*}
\lambda\mapsto L(\lambda)
\end{align*}
is both surjective onto irreducible finite-dimensional modules and injective on isomorphism classes. This is exactly the claimed bijection.
[/guided]
[/step]
[step:Apply the Weyl character formula to compute formal characters]
Let $\lambda\in P^+$. The theorem [citetheorem:9384] applies because the present hypotheses specify the same root datum: the finite-dimensional complex semisimple Lie algebra $\mathfrak g$, Cartan subalgebra $\mathfrak h$, root system $\Phi$, positive system $\Phi^+$, Weyl group $W$, and dominant integral weight $\lambda$. It gives
\begin{align*}
\operatorname{ch}L(\lambda)=
\frac{\sum_{w\in W}(-1)^{\ell(w)}e^{w(\lambda+\rho)}}
{\sum_{w\in W}(-1)^{\ell(w)}e^{w\rho}}.
\end{align*}
This is the asserted character formula.
[/step]
[step:Apply the Weyl dimension formula to compute dimensions]
Let $\lambda\in P^+$. Since $\mathfrak g$, $\mathfrak h$, $\Phi^+$, and the simple-root datum are as in the statement, the hypotheses of [citetheorem:9385] are satisfied. Therefore
\begin{align*}
\dim L(\lambda)=\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}.
\end{align*}
This proves the asserted dimension formula.
[/step]
[step:Identify the dual by its highest weight]
Let $\lambda\in P^+$. By the classification step, $L(\lambda)$ is an irreducible finite-dimensional highest-weight module with dominant integral highest weight $\lambda$. The theorem [citetheorem:9391] applies in this setting, since the chosen positive roots determine the longest Weyl group element $w_0$. It gives an isomorphism of $\mathfrak g$-modules
\begin{align*}
L(\lambda)^*\cong L(-w_0\lambda).
\end{align*}
In particular, $-w_0\lambda$ is dominant integral, as required for the right-hand side to be one of the classified modules.
[/step]
[step:Recover tensor product multiplicities from character multiplication]
Let $\lambda,\mu\in P^+$. The tensor product $L(\lambda)\otimes L(\mu)$ is finite-dimensional. By Weyl complete reducibility for finite-dimensional modules over complex semisimple Lie algebras (citing a result not yet in the wiki: [Weyl complete reducibility theorem](/theorems/3817)), it decomposes as a finite [direct sum](/page/Direct%20Sum) of irreducible finite-dimensional $\mathfrak g$-modules. By the classification already proved, there are uniquely determined nonnegative integers $c_{\lambda\mu}^{\nu}$, all but finitely many equal to $0$, such that
\begin{align*}
L(\lambda)\otimes L(\mu)\cong \bigoplus_{\nu\in P^+}L(\nu)^{\oplus c_{\lambda\mu}^{\nu}}.
\end{align*}
Taking formal characters and using additivity on direct sums gives
\begin{align*}
\operatorname{ch}(L(\lambda)\otimes L(\mu))
=
\sum_{\nu\in P^+}c_{\lambda\mu}^{\nu}\operatorname{ch}L(\nu).
\end{align*}
By [citetheorem:9387], the character of a tensor product is the product of the characters, so
\begin{align*}
\operatorname{ch}L(\lambda)\operatorname{ch}L(\mu)
=
\sum_{\nu\in P^+}c_{\lambda\mu}^{\nu}\operatorname{ch}L(\nu).
\end{align*}
Finally, [citetheorem:9388] says precisely that these multiplicities are uniquely determined by this expansion in the irreducible character basis. Hence tensor products are determined by character multiplication and expansion into irreducible characters. This completes the proof of all assertions.
[/step]
