This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )