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=Poly1R
Assertion ply1ring RRingPRing

Proof

Step Hyp Ref Expression
1 ply1ring.p P=Poly1R
2 eqid PwSer1R=PwSer1R
3 eqid BaseP=BaseP
4 1 2 3 ply1bas BaseP=Base1𝑜mPolyR
5 1 2 3 ply1subrg RRingBasePSubRingPwSer1R
6 4 5 eqeltrrid RRingBase1𝑜mPolyRSubRingPwSer1R
7 1 2 ply1val P=PwSer1R𝑠Base1𝑜mPolyR
8 7 subrgring Base1𝑜mPolyRSubRingPwSer1RPRing
9 6 8 syl RRingPRing