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	|- S = ( Poly1 ` R )
	subrgply1.h	|- H = ( R |`s T )
	subrgply1.u	|- U = ( Poly1 ` H )
	subrgply1.b	|- B = ( Base ` U )
Assertion	subrgply1	|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) )

Proof

Step	Hyp	Ref	Expression
1		subrgply1.s	|- S = ( Poly1 ` R )
2		subrgply1.h	|- H = ( R |`s T )
3		subrgply1.u	|- U = ( Poly1 ` H )
4		subrgply1.b	|- B = ( Base ` U )
5		1on	|- 1o e. On
6		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
7		eqid	|- ( 1o mPoly H ) = ( 1o mPoly H )
8	3 4	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
9	6 2 7 8	subrgmpl	|- ( ( 1o e. On /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` ( 1o mPoly R ) ) )
10	5 9	mpan	|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` ( 1o mPoly R ) ) )
11		eqidd	|- ( T e. ( SubRing ` R ) -> ( Base ` S ) = ( Base ` S ) )
12		eqid	|- ( Base ` S ) = ( Base ` S )
13	1 12	ply1bas	|- ( Base ` S ) = ( Base ` ( 1o mPoly R ) )
14	13	a1i	|- ( T e. ( SubRing ` R ) -> ( Base ` S ) = ( Base ` ( 1o mPoly R ) ) )
15		eqid	|- ( +g ` S ) = ( +g ` S )
16	1 6 15	ply1plusg	|- ( +g ` S ) = ( +g ` ( 1o mPoly R ) )
17	16	a1i	|- ( T e. ( SubRing ` R ) -> ( +g ` S ) = ( +g ` ( 1o mPoly R ) ) )
18	17	oveqdr	|- ( ( T e. ( SubRing ` R ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) )
19		eqid	|- ( .r ` S ) = ( .r ` S )
20	1 6 19	ply1mulr	|- ( .r ` S ) = ( .r ` ( 1o mPoly R ) )
21	20	a1i	|- ( T e. ( SubRing ` R ) -> ( .r ` S ) = ( .r ` ( 1o mPoly R ) ) )
22	21	oveqdr	|- ( ( T e. ( SubRing ` R ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( .r ` S ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) )
23	11 14 18 22	subrgpropd	|- ( T e. ( SubRing ` R ) -> ( SubRing ` S ) = ( SubRing ` ( 1o mPoly R ) ) )
24	10 23	eleqtrrd	|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) )