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 ( PwSer1𝑅 ) = ( PwSer1𝑅 )
3 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
4 1 2 3 ply1bas ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
5 1 2 3 ply1subrg ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) )
6 4 5 eqeltrrid ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) )
7 1 2 ply1val 𝑃 = ( ( PwSer1𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
8 7 subrgring ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1𝑅 ) ) → 𝑃 ∈ Ring )
9 6 8 syl ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )