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	3 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
9	6 2 7 8	subrgmpl	⊢ ( ( 1o ∈ On ∧ 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
10	5 9	mpan	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
11		eqidd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13	1 12	ply1bas	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
14	13	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
15		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
16	1 6 15	ply1plusg	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
17	16	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
18	17	oveqdr	⊢ ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
19		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
20	1 6 19	ply1mulr	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
21	20	a1i	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑆 ) = ( .r ‘ ( 1o mPoly 𝑅 ) ) )
22	21	oveqdr	⊢ ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
23	11 14 18 22	subrgpropd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( SubRing ‘ 𝑆 ) = ( SubRing ‘ ( 1o mPoly 𝑅 ) ) )
24	10 23	eleqtrrd	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )