Metamath Proof Explorer

Theorem subrgpsr

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

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

Proof

Step Hyp Ref Expression
1 subrgpsr.s 
 |-  S = ( I mPwSer R )
2 subrgpsr.h 
 |-  H = ( R |`s T )
3 subrgpsr.u 
 |-  U = ( I mPwSer H )
4 subrgpsr.b 
 |-  B = ( Base ` U )
5 simpl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> I e. V )
6 subrgrcl 
 |-  ( T e. ( SubRing ` R ) -> R e. Ring )
7 6 adantl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> R e. Ring )
8 1 5 7 psrring 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> S e. Ring )
9 2 subrgring 
 |-  ( T e. ( SubRing ` R ) -> H e. Ring )
10 9 adantl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> H e. Ring )
11 3 5 10 psrring 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> U e. Ring )
12 4 a1i 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( Base ` U ) )
13 eqid 
 |-  ( S |`s B ) = ( S |`s B )
14 simpr 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> T e. ( SubRing ` R ) )
15 1 2 3 4 13 14 resspsrbas 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( Base ` ( S |`s B ) ) )
16 1 2 3 4 13 14 resspsradd 
 |-  ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` U ) y ) = ( x ( +g ` ( S |`s B ) ) y ) )
17 1 2 3 4 13 14 resspsrmul 
 |-  ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` U ) y ) = ( x ( .r ` ( S |`s B ) ) y ) )
18 12 15 16 17 ringpropd 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( U e. Ring <-> ( S |`s B ) e. Ring ) )
19 11 18 mpbid 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( S |`s B ) e. Ring )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 13 20 ressbasss 
 |-  ( Base ` ( S |`s B ) ) C_ ( Base ` S )
22 15 21 eqsstrdi 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B C_ ( Base ` S ) )
23 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
27 1 5 7 23 24 25 26 psr1 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
28 25 subrg1cl 
 |-  ( T e. ( SubRing ` R ) -> ( 1r ` R ) e. T )
29 subrgsubg 
 |-  ( T e. ( SubRing ` R ) -> T e. ( SubGrp ` R ) )
30 24 subg0cl 
 |-  ( T e. ( SubGrp ` R ) -> ( 0g ` R ) e. T )
31 29 30 syl 
 |-  ( T e. ( SubRing ` R ) -> ( 0g ` R ) e. T )
32 28 31 ifcld 
 |-  ( T e. ( SubRing ` R ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. T )
33 32 adantl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. T )
34 2 subrgbas 
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
35 34 adantl 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> T = ( Base ` H ) )
36 33 35 eleqtrd 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` H ) )
37 36 adantr 
 |-  ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` H ) )
38 27 37 fmpt3d 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
39 fvex 
 |-  ( Base ` H ) e. _V
40 ovex 
 |-  ( NN0 ^m I ) e. _V
41 40 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
42 39 41 elmap 
 |-  ( ( 1r ` S ) e. ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> ( 1r ` S ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) )
43 38 42 sylibr 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) e. ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
44 eqid 
 |-  ( Base ` H ) = ( Base ` H )
45 3 44 23 4 5 psrbas 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
46 43 45 eleqtrrd 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) e. B )
47 22 46 jca 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) )
48 20 26 issubrg 
 |-  ( B e. ( SubRing ` S ) <-> ( ( S e. Ring /\ ( S |`s B ) e. Ring ) /\ ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) ) )
49 8 19 47 48 syl21anbrc 
 |-  ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` S ) )