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