Theorem subrgply1

Description: A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	subrgply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
	subrgply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	subrgply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
Assertion	subrgply1	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
2		subrgply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		subrgply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4		subrgply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		1on	⊢ 1o ∈ On
6		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
7		eqid	⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
8		eqid	⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
9	3 8 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
10	6 2 7 9	subrgmpl	⊢ ( ( 1o ∈ On ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
11	5 10	mpan	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
12		eqidd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
13		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
14		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
15	1 13 14	ply1bas	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
16	15	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
17		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
18	1 6 17	ply1plusg	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
19	18	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
20	19	oveqdr	⊢ ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
21		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
22	1 6 21	ply1mulr	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
23	22	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑆 ) = ( .r ‘ ( 1o mPoly 𝑅 ) ) )
24	23	oveqdr	⊢ ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
25	12 16 20 24	subrgpropd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( SubRing ‘ 𝑆 ) = ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
26	11 25	eleqtrrd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )