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

Metamath Proof Explorer

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 ⊢ φ → I ∈ V
mplcrngd.r ⊢ φ → R ∈ CRing
Assertion mplcrngd ⊢ φ → P ∈ CRing

Proof

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