Metamath Proof Explorer

Theorem psrgrp

Description: The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Hypotheses psrgrp.s 
|- S = ( I mPwSer R )
psrgrp.i 
|- ( ph -> I e. V )
psrgrp.r 
|- ( ph -> R e. Grp )
Assertion psrgrp 
|- ( ph -> S e. Grp )

Proof

Step Hyp Ref Expression
1 psrgrp.s 
 |-  S = ( I mPwSer R )
2 psrgrp.i 
 |-  ( ph -> I e. V )
3 psrgrp.r 
 |-  ( ph -> R e. Grp )
4 ovex 
 |-  ( NN0 ^m I ) e. _V
5 4 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
6 eqid 
 |-  ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
7 6 pwsgrp 
 |-  ( ( R e. Grp /\ { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V ) -> ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) e. Grp )
8 3 5 7 sylancl 
 |-  ( ph -> ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) e. Grp )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 6 9 pwsbas 
 |-  ( ( R e. Grp /\ { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V ) -> ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
11 3 5 10 sylancl 
 |-  ( ph -> ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
12 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 1 9 12 13 2 psrbas 
 |-  ( ph -> ( Base ` S ) = ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
15 14 eqcomd 
 |-  ( ph -> ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) = ( Base ` S ) )
16 eqid 
 |-  ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) = ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
17 3 adantr 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> R e. Grp )
18 5 a1i 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
19 11 eleq2d 
 |-  ( ph -> ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> x e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) )
20 19 biimpa 
 |-  ( ( ph /\ x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) -> x e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
21 20 adantrr 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> x e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
22 11 eleq2d 
 |-  ( ph -> ( y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> y e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) )
23 22 biimpa 
 |-  ( ( ph /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) -> y e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
24 23 adantrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> y e. ( Base ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
25 eqid 
 |-  ( +g ` R ) = ( +g ` R )
26 eqid 
 |-  ( +g ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) = ( +g ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
27 6 16 17 18 21 24 25 26 pwsplusgval 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> ( x ( +g ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) y ) = ( x oF ( +g ` R ) y ) )
28 eqid 
 |-  ( +g ` S ) = ( +g ` S )
29 14 eleq2d 
 |-  ( ph -> ( x e. ( Base ` S ) <-> x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
30 29 biimpar 
 |-  ( ( ph /\ x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) -> x e. ( Base ` S ) )
31 30 adantrr 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> x e. ( Base ` S ) )
32 14 eleq2d 
 |-  ( ph -> ( y e. ( Base ` S ) <-> y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) )
33 32 biimpar 
 |-  ( ( ph /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) -> y e. ( Base ` S ) )
34 33 adantrl 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> y e. ( Base ` S ) )
35 1 13 25 28 31 34 psradd 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> ( x ( +g ` S ) y ) = ( x oF ( +g ` R ) y ) )
36 27 35 eqtr4d 
 |-  ( ( ph /\ ( x e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ y e. ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) ) -> ( x ( +g ` ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) y ) = ( x ( +g ` S ) y ) )
37 11 15 36 grppropd 
 |-  ( ph -> ( ( R ^s { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) e. Grp <-> S e. Grp ) )
38 8 37 mpbid 
 |-  ( ph -> S e. Grp )