Metamath Proof Explorer


Theorem gsummptfidmsub

Description: The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses gsummptfidmsub.b B = Base G
gsummptfidmsub.s - ˙ = - G
gsummptfidmsub.g φ G Abel
gsummptfidmsub.a φ A Fin
gsummptfidmsub.c φ x A C B
gsummptfidmsub.d φ x A D B
gsummptfidmsub.f F = x A C
gsummptfidmsub.h H = x A D
Assertion gsummptfidmsub φ G x A C - ˙ D = G F - ˙ G H

Proof

Step Hyp Ref Expression
1 gsummptfidmsub.b B = Base G
2 gsummptfidmsub.s - ˙ = - G
3 gsummptfidmsub.g φ G Abel
4 gsummptfidmsub.a φ A Fin
5 gsummptfidmsub.c φ x A C B
6 gsummptfidmsub.d φ x A D B
7 gsummptfidmsub.f F = x A C
8 gsummptfidmsub.h H = x A D
9 eqid 0 G = 0 G
10 7 a1i φ F = x A C
11 8 a1i φ H = x A D
12 fvexd φ 0 G V
13 7 4 5 12 fsuppmptdm φ finSupp 0 G F
14 8 4 6 12 fsuppmptdm φ finSupp 0 G H
15 1 9 2 3 4 5 6 10 11 13 14 gsummptfssub φ G x A C - ˙ D = G F - ˙ G H