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 ⊢ P = I mPoly R
mplringd.i ⊢ φ → I ∈ V
mplringd.r ⊢ φ → R ∈ Ring
Assertion mplringd ⊢ φ → P ∈ Ring

Proof

Step Hyp Ref Expression
1 mplringd.p ⊢ P = I mPoly R
2 mplringd.i ⊢ φ → I ∈ V
3 mplringd.r ⊢ φ → R ∈ Ring
4 1 mplring ⊢ I ∈ V ∧ R ∈ Ring → P ∈ Ring
5 2 3 4 syl2anc ⊢ φ → P ∈ Ring