Metamath Proof Explorer


Theorem ply1ring

Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypothesis ply1ring.p P = Poly 1 R
Assertion ply1ring R Ring P Ring

Proof

Step Hyp Ref Expression
1 ply1ring.p P = Poly 1 R
2 eqid Base P = Base P
3 1 2 ply1bas Base P = Base 1 𝑜 mPoly R
4 eqid PwSer 1 R = PwSer 1 R
5 1 4 2 ply1subrg R Ring Base P SubRing PwSer 1 R
6 3 5 eqeltrrid R Ring Base 1 𝑜 mPoly R SubRing PwSer 1 R
7 1 4 ply1val P = PwSer 1 R 𝑠 Base 1 𝑜 mPoly R
8 7 subrgring Base 1 𝑜 mPoly R SubRing PwSer 1 R P Ring
9 6 8 syl R Ring P Ring