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 ˙ = 0 G
gsumzinv.z Z = Cntz G
gsumzinv.i I = inv g G
gsumzinv.g φ G Grp
gsumzinv.a φ A V
gsumzinv.f φ F : A B
gsumzinv.c φ ran F Z ran F
gsumzinv.n φ finSupp 0 ˙ F
Assertion gsumzinv φ G I F = I G F

Proof

Step Hyp Ref Expression
1 gsumzinv.b B = Base G
2 gsumzinv.0 0 ˙ = 0 G
3 gsumzinv.z Z = Cntz G
4 gsumzinv.i I = inv g G
5 gsumzinv.g φ G Grp
6 gsumzinv.a φ A V
7 gsumzinv.f φ F : A B
8 gsumzinv.c φ ran F Z ran F
9 gsumzinv.n φ finSupp 0 ˙ F
10 eqid opp 𝑔 G = opp 𝑔 G
11 5 grpmndd φ G Mnd
12 1 4 grpinvf G Grp I : B B
13 5 12 syl φ I : B B
14 fco I : B B F : A B I F : A B
15 13 7 14 syl2anc φ I F : A B
16 10 4 invoppggim G Grp I G GrpIso opp 𝑔 G
17 gimghm I G GrpIso opp 𝑔 G I G GrpHom opp 𝑔 G
18 ghmmhm I G GrpHom opp 𝑔 G I G MndHom opp 𝑔 G
19 5 16 17 18 4syl φ I G MndHom opp 𝑔 G
20 eqid Cntz opp 𝑔 G = Cntz opp 𝑔 G
21 3 20 cntzmhm2 I G MndHom opp 𝑔 G ran F Z ran F I ran F Cntz opp 𝑔 G I ran F
22 19 8 21 syl2anc φ I ran F Cntz opp 𝑔 G I ran F
23 rnco2 ran I F = I ran F
24 23 fveq2i Z ran I F = Z I ran F
25 10 3 oppgcntz Z I ran F = Cntz opp 𝑔 G I ran F
26 24 25 eqtri Z ran I F = Cntz opp 𝑔 G I ran F
27 22 23 26 3sstr4g φ ran I F Z ran I F
28 2 fvexi 0 ˙ V
29 28 a1i φ 0 ˙ V
30 1 fvexi B V
31 30 a1i φ B V
32 2 4 grpinvid G Grp I 0 ˙ = 0 ˙
33 5 32 syl φ I 0 ˙ = 0 ˙
34 29 7 13 6 31 9 33 fsuppco2 φ finSupp 0 ˙ I F
35 1 2 3 10 11 6 15 27 34 gsumzoppg φ opp 𝑔 G I F = G I F
36 10 oppgmnd G Mnd opp 𝑔 G Mnd
37 11 36 syl φ opp 𝑔 G Mnd
38 1 3 11 37 6 19 7 8 2 9 gsumzmhm φ opp 𝑔 G I F = I G F
39 35 38 eqtr3d φ G I F = I G F