Theorem mplringd

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

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

Proof

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