Resultant nonzero for polynomials coprime over the fraction field

Let $P$ and $Q$ be univariate polynomials over the coefficient ring $\mathrm{XCoeff} = \mathrm{MvPolynomial}\,(\mathrm{Fin}\,1)\,\mathbb{R}$, and assume coprimality after base change to its fraction field, $h_{cop} : \mathrm{IsCoprime}\,(P.\mathrm{map}\,\mathrm{algebraMap})\,(Q.\mathrm{map}\,\mathrm{algebraMap})$ over $\mathrm{XFrac} = \mathrm{FractionRing}\,\mathrm{XCoeff}$. Then their resultant is nonzero:

This is the abstract resultant criterion: coprimality over a field (here the fraction field of the UFD $\mathrm{XCoeff}$) forces a nonzero resultant, since the Sylvester determinant detects a common factor. It is the bridge from the fraction-field coprimality obtained via primitivity lemmas to the concrete nonvanishing of the resultant polynomial whose roots are then counted.