Weyl anti invariants are divisible by the discriminant

Let $p\in S^{\det }$ and let ${\mathrm{\ell }}_{\alpha }$ be any factor of $\mathrm{\Delta }$. On its reflecting hyperplane $s_{\alpha }v=v$, so $p(v)=p(s_{\alpha }v)=-p(v)$ and therefore $p(v)=0$. Extend ${\mathrm{\ell }}_{\alpha }$ to a linear coordinate system $x_1={\mathrm{\ell }}_{\alpha },x_2,\dots ,x_r$. The constant coefficient in $x_1$ vanishes at every $(x_2,\dots ,x_r)$, hence is the zero polynomial by F2's polynomial-function faithfulness. Thus ${\mathrm{\ell }}_{\alpha }$ divides $p$.

In a polynomial ring over a field a nonzero product is nonzero: choose, for example, the lexicographically highest monomial of each factor, whose product is the unique highest monomial of the product and has nonzero coefficient. Also the ideal generated by a nonzero linear form is prime, since a linear coordinate change identifies its quotient with a polynomial ring in one fewer variable, which is a domain by that same argument. Two nonproportional linear forms do not divide each other, since a quotient between degree-one polynomials would have degree zero. Consequently if each of finitely many pairwise nonproportional linear forms divides $p$, their product divides $p$: induct, and use primeness to divide the remaining quotient by the next factor, since it divides none of the preceding factors. These statements include $p=0$ by taking quotient zero.

Steps 1.1–1.2 give $p=\mathrm{\Delta }q$. For $w\in W$, F1 and anti-invariance yield $\det (w)\mathrm{\Delta }(w\cdot q)=w\cdot p=\det (w)\mathrm{\Delta }q$. The determinant is nonzero and the polynomial ring is a domain, so $w\cdot q=q$. Thus $q\in S^W$, and domain cancellation also proves uniqueness. Conversely if $q$ is invariant, F1 gives $w\cdot (\mathrm{\Delta }q)=\det (w)\mathrm{\Delta }q$, so it is anti-invariant. When the rank is zero, $\mathrm{\Delta }=1$ and both sides are $\mathbb{C}$. All coordinate extensions and products are finite, so no AC enters.