Metamath Proof Explorer

Theorem gsumzinv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumzinv.b 
|- B = ( Base ` G )
gsumzinv.0 
|- .0. = ( 0g ` G )
gsumzinv.z 
|- Z = ( Cntz ` G )
gsumzinv.i 
|- I = ( invg ` G )
gsumzinv.g 
|- ( ph -> G e. Grp )
gsumzinv.a 
|- ( ph -> A e. V )
gsumzinv.f 
|- ( ph -> F : A --> B )
gsumzinv.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzinv.n 
|- ( ph -> F finSupp .0. )
Assertion gsumzinv 
|- ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )

Proof

Step Hyp Ref Expression
1 gsumzinv.b 
 |-  B = ( Base ` G )
2 gsumzinv.0 
 |-  .0. = ( 0g ` G )
3 gsumzinv.z 
 |-  Z = ( Cntz ` G )
4 gsumzinv.i 
 |-  I = ( invg ` G )
5 gsumzinv.g 
 |-  ( ph -> G e. Grp )
6 gsumzinv.a 
 |-  ( ph -> A e. V )
7 gsumzinv.f 
 |-  ( ph -> F : A --> B )
8 gsumzinv.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
9 gsumzinv.n 
 |-  ( ph -> F finSupp .0. )
10 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
11 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
12 5 11 syl 
 |-  ( ph -> G e. Mnd )
13 1 4 grpinvf 
 |-  ( G e. Grp -> I : B --> B )
14 5 13 syl 
 |-  ( ph -> I : B --> B )
15 fco 
 |-  ( ( I : B --> B /\ F : A --> B ) -> ( I o. F ) : A --> B )
16 14 7 15 syl2anc 
 |-  ( ph -> ( I o. F ) : A --> B )
17 10 4 invoppggim 
 |-  ( G e. Grp -> I e. ( G GrpIso ( oppG ` G ) ) )
18 gimghm 
 |-  ( I e. ( G GrpIso ( oppG ` G ) ) -> I e. ( G GrpHom ( oppG ` G ) ) )
19 ghmmhm 
 |-  ( I e. ( G GrpHom ( oppG ` G ) ) -> I e. ( G MndHom ( oppG ` G ) ) )
20 5 17 18 19 4syl 
 |-  ( ph -> I e. ( G MndHom ( oppG ` G ) ) )
21 eqid 
 |-  ( Cntz ` ( oppG ` G ) ) = ( Cntz ` ( oppG ` G ) )
22 3 21 cntzmhm2 
 |-  ( ( I e. ( G MndHom ( oppG ` G ) ) /\ ran F C_ ( Z ` ran F ) ) -> ( I " ran F ) C_ ( ( Cntz ` ( oppG ` G ) ) ` ( I " ran F ) ) )
23 20 8 22 syl2anc 
 |-  ( ph -> ( I " ran F ) C_ ( ( Cntz ` ( oppG ` G ) ) ` ( I " ran F ) ) )
24 rnco2 
 |-  ran ( I o. F ) = ( I " ran F )
25 24 fveq2i 
 |-  ( Z ` ran ( I o. F ) ) = ( Z ` ( I " ran F ) )
26 10 3 oppgcntz 
 |-  ( Z ` ( I " ran F ) ) = ( ( Cntz ` ( oppG ` G ) ) ` ( I " ran F ) )
27 25 26 eqtri 
 |-  ( Z ` ran ( I o. F ) ) = ( ( Cntz ` ( oppG ` G ) ) ` ( I " ran F ) )
28 23 24 27 3sstr4g 
 |-  ( ph -> ran ( I o. F ) C_ ( Z ` ran ( I o. F ) ) )
29 2 fvexi 
 |-  .0. e. _V
30 29 a1i 
 |-  ( ph -> .0. e. _V )
31 1 fvexi 
 |-  B e. _V
32 31 a1i 
 |-  ( ph -> B e. _V )
33 2 4 grpinvid 
 |-  ( G e. Grp -> ( I ` .0. ) = .0. )
34 5 33 syl 
 |-  ( ph -> ( I ` .0. ) = .0. )
35 30 7 14 6 32 9 34 fsuppco2 
 |-  ( ph -> ( I o. F ) finSupp .0. )
36 1 2 3 10 12 6 16 28 35 gsumzoppg 
 |-  ( ph -> ( ( oppG ` G ) gsum ( I o. F ) ) = ( G gsum ( I o. F ) ) )
37 10 oppgmnd 
 |-  ( G e. Mnd -> ( oppG ` G ) e. Mnd )
38 12 37 syl 
 |-  ( ph -> ( oppG ` G ) e. Mnd )
39 1 3 12 38 6 20 7 8 2 9 gsumzmhm 
 |-  ( ph -> ( ( oppG ` G ) gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )
40 36 39 eqtr3d 
 |-  ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )