Simple root power relations generate the integrable quotient

Put $u_i=f_i^{m_i+1}v$. From F6, $h_i{f}_i^{r}v=(m_i-2r)f_i^{r}v$. Starting with $e_{i}v=0$, the recurrence $e_i{f}_i^{r+1}v=f_i{e}_i{f}_i^{r}v+h_i{f}_i^{r}v$ gives $e_i{f}_i^{r}v=r(m_i-r+1)f_i^{r-1}v$ by induction; substituting $r=m_i+1$ gives $e_i{u}_i=0$. If $j\mathrm{\ne }i$, F6 gives $[e_j,f_i]=0$, hence $e_j{u}_i=f_i^{m_i+1}{e}_{j}v=0$. Thus every simple raising generator kills $u_i$, and so does their generated algebra ${\mathfrak{n}}^{+}$. Its weight is $\lambda -(m_i+1){\alpha }_i$ by F6. Universality and negative PBW spanning in F1 imply that $U(\mathfrak{g})u_i$ has support in $\lambda -(m_i+1){\alpha }_i-Q^{+}$, even if $u_i=0$. Since $m_i+1>0$, this cone misses $\lambda$. Therefore their sum $N$ misses the one-dimensional top. By F5 the quotient is a weight module, and its surviving top vector $\bar{v}$ generates it; in particular it is nonzero.

Fix $i$ and put $D=\mathrm{ad}{f}_i$ on $U(\mathfrak{g})$. On Lie generators its nilpotence follows from F4 and F6: $D^{1-a_{ij}}{f}_j=0$ for $j\mathrm{\ne }i$, $D{f}_i=0$, $D{e}_j=0$ for $j\mathrm{\ne }i$, $D{e}_i=-h_i$, $D^2{e}_i=-2f_i$, $D^3{e}_i=0$, and $D^{2}h=0$. These Lie generators also generate the enveloping algebra as an associative algebra. In the enveloping algebra, induction using the derivation rule and Pascal addition gives $D^r(ab)={\sum }_{k=0}^r\left(\genfrac{}{}{0px}{}{r}{k}\right)D^k(a)D^{r-k}(b)$. If $D^{p}a=0$ and $D^{q}b=0$, every summand vanishes for $r\ge p+q-1$. Induction on product length and a maximum for finite sums show that for each $u\in U(\mathfrak{g})$ there is $K\ge 1$ with $D^{K}u=0$.

On a quotient weight vector of weight $\lambda -\beta$, write $\beta ={\sum }_j{b}_j{\alpha }_j\in Q^{+}$. Applying $e_i^{b_i+1}$ would give weight $\lambda -\beta +(b_i+1){\alpha }_i$, outside $\lambda -Q^{+}$ because its $i$-coordinate difference is $-1$. The quotient support is contained in that cone by F1 and 1.1, so this power vanishes. Taking the maximum exponent over the finitely many weight components of a vector proves local nilpotence of every $e_i$.

In any associative algebra, $f_i^{r}u={\sum }_{k=0}^r\left(\genfrac{}{}{0px}{}{r}{k}\right)D^k(u)f_i^{r-k}$. For $r=0$ the assertion is $u=u$; multiplication on the left by $f_i$, followed by $f_{i}a=D(a)+a{f}_i$ and Pascal addition, proves the induction step. Apply this identity to $\bar{v}$ and take $r=K+m_i$, where $K$ is from 1.2. Terms with $k\ge K$ vanish because $D^{k}u=0$. For $k<K$, $r-k\ge m_i+1$ and the defining relation $f_i^{m_i+1}\bar{v}=0$ kills the term. Every quotient vector is $u\bar{v}$ for some $u$, so $f_i$ is locally nilpotent.

The weight decomposition in 1.1 and both nilpotence conclusions give integrability by F3. If $m_i=0$, the imposed relation is $f_i\bar{v}=0$ and the same bound is $r=K$. For $u=0$ choose $K=1$. Empty sets of simple roots impose no relations and give the one-dimensional Cartan Verma module by F1. All sums defining elements, polynomial expansions and bounds are finite; no AC or assertion that Serre elements generate a defining ideal enters.