Theorem mplcrngd

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

	Ref	Expression
Hypotheses	mplcrngd.p	|- P = ( I mPoly R )
	mplcrngd.i	|- ( ph -> I e. V )
	mplcrngd.r	|- ( ph -> R e. CRing )
Assertion	mplcrngd	|- ( ph -> P e. CRing )

Proof

Step	Hyp	Ref	Expression
1		mplcrngd.p	|- P = ( I mPoly R )
2		mplcrngd.i	|- ( ph -> I e. V )
3		mplcrngd.r	|- ( ph -> R e. CRing )
4	1	mplcrng	|- ( ( I e. V /\ R e. CRing ) -> P e. CRing )
5	2 3 4	syl2anc	|- ( ph -> P e. CRing )