This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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