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 )