Metamath Proof Explorer

Theorem psrgrp

Description: The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014)

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 eqidd 
 |-  ( ph -> ( Base ` S ) = ( Base ` S ) )
5 eqidd 
 |-  ( ph -> ( +g ` S ) = ( +g ` S ) )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( +g ` S ) = ( +g ` S )
8 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Grp )
9 simp2 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) )
10 simp3 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
11 1 6 7 8 9 10 psraddcl 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 12 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
14 13 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
17 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
18 1 15 16 6 17 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
19 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
20 1 15 16 6 19 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
21 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
22 1 15 16 6 21 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
23 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Grp )
24 eqid 
 |-  ( +g ` R ) = ( +g ` R )
25 15 24 grpass 
 |-  ( ( R e. Grp /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( +g ` R ) t ) = ( r ( +g ` R ) ( s ( +g ` R ) t ) ) )
26 23 25 sylan 
 |-  ( ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( +g ` R ) t ) = ( r ( +g ` R ) ( s ( +g ` R ) t ) ) )
27 14 18 20 22 26 caofass 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
28 1 6 24 7 17 19 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) = ( x oF ( +g ` R ) y ) )
29 28 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) = ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) )
30 1 6 24 7 19 21 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) = ( y oF ( +g ` R ) z ) )
31 30 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
32 27 29 31 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) = ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) )
33 11 3adant3r3 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
34 1 6 24 7 33 21 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( +g ` S ) z ) = ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) )
35 1 6 7 23 19 21 psraddcl 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) e. ( Base ` S ) )
36 1 6 24 7 17 35 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) ( y ( +g ` S ) z ) ) = ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) )
37 32 34 36 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( +g ` S ) z ) = ( x ( +g ` S ) ( y ( +g ` S ) z ) ) )
38 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
39 1 2 3 16 38 6 psr0cl 
 |-  ( ph -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) e. ( Base ` S ) )
40 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> I e. V )
41 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> R e. Grp )
42 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
43 1 40 41 16 38 6 7 42 psr0lid 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) ( +g ` S ) x ) = x )
44 eqid 
 |-  ( invg ` R ) = ( invg ` R )
45 1 40 41 16 44 6 42 psrnegcl 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( invg ` R ) o. x ) e. ( Base ` S ) )
46 1 40 41 16 44 6 42 38 7 psrlinv 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( ( invg ` R ) o. x ) ( +g ` S ) x ) = ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) )
47 4 5 11 37 39 43 45 46 isgrpd 
 |-  ( ph -> S e. Grp )