This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )