Theorem mplcrngd

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

	Ref	Expression
Hypotheses	mplcrngd.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplcrngd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplcrngd.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	mplcrngd	⊢ ( 𝜑 → 𝑃 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		mplcrngd.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplcrngd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		mplcrngd.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4	1	mplcrng	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ CRing )
5	2 3 4	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ CRing )