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