Metamath Proof Explorer

Theorem subrgmpl

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

Ref Expression
Hypotheses subrgmpl.s 
|- S = ( I mPoly R )
subrgmpl.h 
|- H = ( R |`s T )
subrgmpl.u 
|- U = ( I mPoly H )
subrgmpl.b 
|- B = ( Base ` U )
Assertion subrgmpl 
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` S ) )

Proof

Step Hyp Ref Expression
1 subrgmpl.s 
 |-  S = ( I mPoly R )
2 subrgmpl.h 
 |-  H = ( R |`s T )
3 subrgmpl.u 
 |-  U = ( I mPoly H )
4 subrgmpl.b 
 |-  B = ( Base ` U )
5 simpl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> I e. V )
6 simpr 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> T e. ( SubRing ` R ) )
7 eqid 
 |-  ( I mPwSer H ) = ( I mPwSer H )
8 eqid 
 |-  ( Base ` ( I mPwSer H ) ) = ( Base ` ( I mPwSer H ) )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 1 2 3 4 5 6 7 8 9 ressmplbas2 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) )
11 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
12 11 2 7 8 subrgpsr 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( Base ` ( I mPwSer H ) ) e. ( SubRing ` ( I mPwSer R ) ) )
13 subrgrcl 
 |-  ( T e. ( SubRing ` R ) -> R e. Ring )
14 13 adantl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> R e. Ring )
15 11 1 9 5 14 mplsubrg 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( Base ` S ) e. ( SubRing ` ( I mPwSer R ) ) )
16 subrgin 
 |-  ( ( ( Base ` ( I mPwSer H ) ) e. ( SubRing ` ( I mPwSer R ) ) /\ ( Base ` S ) e. ( SubRing ` ( I mPwSer R ) ) ) -> ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) e. ( SubRing ` ( I mPwSer R ) ) )
17 12 15 16 syl2anc 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) e. ( SubRing ` ( I mPwSer R ) ) )
18 10 17 eqeltrd 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` ( I mPwSer R ) ) )
19 inss2 
 |-  ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) C_ ( Base ` S )
20 10 19 eqsstrdi 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B C_ ( Base ` S ) )
21 1 11 9 mplval2 
 |-  S = ( ( I mPwSer R ) |`s ( Base ` S ) )
22 21 subsubrg 
 |-  ( ( Base ` S ) e. ( SubRing ` ( I mPwSer R ) ) -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` ( I mPwSer R ) ) /\ B C_ ( Base ` S ) ) ) )
23 15 22 syl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` ( I mPwSer R ) ) /\ B C_ ( Base ` S ) ) ) )
24 18 20 23 mpbir2and 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` S ) )