Metamath Proof Explorer


Theorem ply1ring

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

Ref Expression
Hypothesis ply1ring.p 𝑃 = ( Poly1𝑅 )
Assertion ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )

Proof

Step Hyp Ref Expression
1 ply1ring.p 𝑃 = ( Poly1𝑅 )
2 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
3 1 2 ply1bas ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
4 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
5 1 4 2 ply1subrg ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) )
6 3 5 eqeltrrid ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) )
7 1 4 ply1val 𝑃 = ( ( PwSer1𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
8 7 subrgring ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) → 𝑃 ∈ Ring )
9 6 8 syl ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )