Metamath Proof Explorer


Theorem gsummptfidminv

Description: Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019)

Ref Expression
Hypotheses gsuminv.b B = Base G
gsuminv.z 0 ˙ = 0 G
gsuminv.p I = inv g G
gsuminv.g φ G Abel
gsummptfidminv.a φ A Fin
gsummptfidminv.c φ x A C B
gsummptfidminv.f F = x A C
Assertion gsummptfidminv φ G I F = I G F

Proof

Step Hyp Ref Expression
1 gsuminv.b B = Base G
2 gsuminv.z 0 ˙ = 0 G
3 gsuminv.p I = inv g G
4 gsuminv.g φ G Abel
5 gsummptfidminv.a φ A Fin
6 gsummptfidminv.c φ x A C B
7 gsummptfidminv.f F = x A C
8 6 7 fmptd φ F : A B
9 2 fvexi 0 ˙ V
10 9 a1i φ 0 ˙ V
11 7 5 6 10 fsuppmptdm φ finSupp 0 ˙ F
12 1 2 3 4 5 8 11 gsuminv φ G I F = I G F