Integrable weight sets and multiplicities are weyl invariant

Put $e=e_i$, $f=f_i$, $h_0=h_i$. Define $T=\exp (f)\exp (-e)\exp (f)$ on $V$, with each exponential evaluated on a vector by its finite power sum, justified by F1. The inverse is $\exp (-f)\exp (e)\exp (-f)$: for a locally nilpotent operator $x$, the coefficient of $x^m$ in $\exp (x)\exp (-x)$ is ${\sum }_{k=0}^m(-1{)}^k\mathrm{/}(k!(m-k)!)$, equal to $1$ for $m=0$ and zero otherwise. Every such multiplication on a vector is finite. Thus $T$ is a well-defined linear automorphism.

On a finite invariant cyclic module from F3, $e$ and $f$ are nilpotent matrices. For a nilpotent matrix $x$, multiplication of the two finite exponential polynomials and the identity $(\mathrm{ad}x{)}^r(y)={\sum }_{k=0}^r(-1{)}^k\left(\genfrac{}{}{0px}{}{r}{k}\right)x^{r-k}y{x}^k$ give $\exp (x)y\exp (-x)={\sum }_r(\mathrm{ad}x{)}^r(y)\mathrm{/}r!$; the identity follows inductively by taking the next commutator. Apply this to the triple matrices. F4 gives conjugation by $\exp (f)$ sending $h_0$ to $h_0+2f$, and conjugation by $\exp (-e)$ sending $h_0$ to $h_0+2e$ and $f$ to $f-h_0-e$. Thus successive conjugations send $h_0$ to $h_0+2f$, then $-h_0+2f$, then $-h_0$. For a weight vector, its cyclic module is invariant under all of $\mathfrak{h}$: commuting a Cartan element through a word in $e,f,h_0$ expresses its action as a scalar on the original weight vector plus words of the same kind. Every $h\in \mathfrak{h}$ splits as $h^{\mathrm{\prime }}=h-{\alpha }_i(h)h_0\mathrm{/}2$ plus ${\alpha }_i(h)h_0\mathrm{/}2$. Since ${\alpha }_i(h^{\mathrm{\prime }})=0$, F4 makes $h^{\mathrm{\prime }}$ commute with $e,f$ and hence with $T$. Consequently $Th{T}^{-1}=h-{\alpha }_i(h)h_0=s_{i}h$ on all weight vectors and therefore on $V$.

By F2, $s_i^2=1$, so 1.2 also gives $T^{-1}hT=s_{i}h$. For $v\in V_{\mu }$, $hTv=T(s_{i}h)v=\mu (s_{i}h)Tv=(s_i\mu )(h)Tv$. Thus $T(V_{\mu })\subseteq V_{s_i\mu }$. Its inverse satisfies the corresponding formula and sends that space into $V_{\mu }$, proving equality and an isomorphism. Compose these maps along any finite expression $w=s_{i_1}\cdots s_{i_r}$. The resulting map is invertible and implements the prescribed weight action; no assertion that different expressions give identical operators is needed.

These isomorphisms preserve vanishing and nonvanishing of weight spaces, proving support invariance. If $B$ is any basis of $V_{\mu }$, its image is independent because applying the inverse to a finite linear relation gives one among $B$; it spans because the inverse of every target vector is a finite combination of $B$. Hence the two spaces have bases in explicit bijection. In the arbitrary-space cardinal interpretation, F5 and F6 supply $B$; this is the sole use of AC. Zero weight spaces have empty bases, a one-dimensional space transports its single basis vector, and the zero module has empty support. An empty Weyl word gives the identity. Zero simple labels mean a preserved weight space, without claiming $T$ acts identically there. The isomorphism and finite-dimensional conclusions used no AC.