Theorem mplcrngd

Description: The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025)

	Ref	Expression
Hypotheses	mplcrngd.p	$$⊢P=I\mathrm{mPoly}R$$
	mplcrngd.i	$$⊢\phi \to I\in V$$
	mplcrngd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
Assertion	mplcrngd	$$⊢\phi \to P\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		mplcrngd.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplcrngd.i	$$⊢\phi \to I\in V$$
3		mplcrngd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4	1	mplcrng	$$⊢\left(I\in V\wedge R\in \mathrm{CRing}\right)\to P\in \mathrm{CRing}$$
5	2 3 4	syl2anc	$$⊢\phi \to P\in \mathrm{CRing}$$