PBW linear independence via the ordered-monomial model

On a basis word, orient every adjacent inversion $yx$ with $y>x$ by the linear rewrite $yx⇝xy+[y,x]$, expanding the bracket in the supplied basis by [F1]. Every resulting term decreases lexicographically in (length, inversion number), so every reduction sequence terminates in a linear combination of ordered words.

Reductions at disjoint adjacent pairs commute after expansion. The only overlapping critical word is $zyx$ with $z>y>x$: reducing its left pair first gives, before lower reductions, $xyz+[y,x]z+y[z,x]+[z,y]x$, whereas reducing its right pair first gives $xyz+x[z,y]+[z,x]y+z[y,x]$. In the outer induction on word length, the difference of their terminal forms is therefore the already-defined normal form of $[[y,x],z]+[y,[z,x]]+[[z,y],x]$, which is zero by the Jacobi identity.

A well-founded induction on the decreasing measure now proves uniqueness of the terminal result: if two reduction sequences start differently, step 2.1 joins their first reductions, and the induction hypothesis identifies the normal forms of all lower terms. Denote the resulting linear normal-form map by $N:T(\mathfrak{g})\to P$. It fixes ordered words and satisfies $N(r(yx-xy-[y,x])s)=0$ in every word context. By bilinearity, alternation, and totality of the order, it kills every defining enveloping relator and hence the ideal they generate.

For $x\in \mathfrak{g}$, define $L_x:P\to P$ by $L_x(p)=N(xp)$, extending from word-basis elements linearly. Context compatibility from step 3.1 gives $N(xN(q))=N(xq)$; consequently $[L_x,L_y](p)=N((xy-yx)p)=N([x,y]p)=L_{[x,y]}(p)$. Thus $x\mapsto L_x$ is a Lie representation.

By [L2], the operators $L_x$ extend to a $U(\mathfrak{g})$-action on $P$. If $b_1\le \cdots \le b_n$, then the ordered product ${\iota }_{\mathfrak{g}}(b_1)\cdots {\iota }_{\mathfrak{g}}(b_n)$ sends the empty word to $b_1\cdots b_n$: acting from the right successively inserts $b_n,b_{n-1},\dots ,b_1$ without an inversion.

Apply any finite linear relation among ordered monomials in $U(\mathfrak{g})$ to the empty word. Step 5.1 turns it into the same linear combination of distinct basis words of $P$, so every coefficient is zero by [L1]. Hence the ordered monomials are linearly independent, including the empty-basis case.