Theorem ply1subrg

Description: Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1val.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
	ply1bas.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
Assertion	ply1subrg	⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1val.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
3		ply1bas.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6	1 2 3	ply1bas	⊢ 𝑈 = ( Base ‘ ( 1o mPoly 𝑅 ) )
7		1on	⊢ 1o ∈ On
8	7	a1i	⊢ ( 𝑅 ∈ Ring → 1o ∈ On )
9		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
10	4 5 6 8 9	mplsubrg	⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( SubRing ‘ ( 1o mPwSer 𝑅 ) ) )
11		eqidd	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
12	2	psr1val	⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
13		0ss	⊢ ∅ ⊆ ( 1o × 1o )
14	13	a1i	⊢ ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) )
15	4 12 14	opsrbas	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ 𝑆 ) )
16	4 12 14	opsrplusg	⊢ ( 𝑅 ∈ Ring → ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g ‘ 𝑆 ) )
17	16	oveqdr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
18	4 12 14	opsrmulr	⊢ ( 𝑅 ∈ Ring → ( .r ‘ ( 1o mPwSer 𝑅 ) ) = ( .r ‘ 𝑆 ) )
19	18	oveqdr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) )
20	11 15 17 19	subrgpropd	⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ ( 1o mPwSer 𝑅 ) ) = ( SubRing ‘ 𝑆 ) )
21	10 20	eleqtrd	⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( SubRing ‘ 𝑆 ) )