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		eqid	|- ( PwSer1 ` H ) = ( PwSer1 ` H )
9	3 8 4	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
10	6 2 7 9	subrgmpl	|- ( ( 1o e. On /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` ( 1o mPoly R ) ) )
11	5 10	mpan	|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` ( 1o mPoly R ) ) )
12		eqidd	|- ( T e. ( SubRing ` R ) -> ( Base ` S ) = ( Base ` S ) )
13		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
14		eqid	|- ( Base ` S ) = ( Base ` S )
15	1 13 14	ply1bas	|- ( Base ` S ) = ( Base ` ( 1o mPoly R ) )
16	15	a1i	|- ( T e. ( SubRing ` R ) -> ( Base ` S ) = ( Base ` ( 1o mPoly R ) ) )
17		eqid	|- ( +g ` S ) = ( +g ` S )
18	1 6 17	ply1plusg	|- ( +g ` S ) = ( +g ` ( 1o mPoly R ) )
19	18	a1i	|- ( T e. ( SubRing ` R ) -> ( +g ` S ) = ( +g ` ( 1o mPoly R ) ) )
20	19	oveqdr	|- ( ( T e. ( SubRing ` R ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) )
21		eqid	|- ( .r ` S ) = ( .r ` S )
22	1 6 21	ply1mulr	|- ( .r ` S ) = ( .r ` ( 1o mPoly R ) )
23	22	a1i	|- ( T e. ( SubRing ` R ) -> ( .r ` S ) = ( .r ` ( 1o mPoly R ) ) )
24	23	oveqdr	|- ( ( T e. ( SubRing ` R ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( .r ` S ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) )
25	12 16 20 24	subrgpropd	|- ( T e. ( SubRing ` R ) -> ( SubRing ` S ) = ( SubRing ` ( 1o mPoly R ) ) )
26	11 25	eleqtrrd	|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) )