Metamath Proof Explorer


Theorem gsummptfssub

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

Ref Expression
Hypotheses gsummptfssub.b B=BaseG
gsummptfssub.z 0˙=0G
gsummptfssub.s -˙=-G
gsummptfssub.g φGAbel
gsummptfssub.a φAV
gsummptfssub.c φxACB
gsummptfssub.d φxADB
gsummptfssub.f φF=xAC
gsummptfssub.h φH=xAD
gsummptfssub.w φfinSupp0˙F
gsummptfssub.v φfinSupp0˙H
Assertion gsummptfssub φGxAC-˙D=GF-˙GH

Proof

Step Hyp Ref Expression
1 gsummptfssub.b B=BaseG
2 gsummptfssub.z 0˙=0G
3 gsummptfssub.s -˙=-G
4 gsummptfssub.g φGAbel
5 gsummptfssub.a φAV
6 gsummptfssub.c φxACB
7 gsummptfssub.d φxADB
8 gsummptfssub.f φF=xAC
9 gsummptfssub.h φH=xAD
10 gsummptfssub.w φfinSupp0˙F
11 gsummptfssub.v φfinSupp0˙H
12 5 6 7 8 9 offval2 φF-˙fH=xAC-˙D
13 12 eqcomd φxAC-˙D=F-˙fH
14 13 oveq2d φGxAC-˙D=GF-˙fH
15 8 6 fmpt3d φF:AB
16 9 7 fmpt3d φH:AB
17 1 2 3 4 5 15 16 10 11 gsumsub φGF-˙fH=GF-˙GH
18 14 17 eqtrd φGxAC-˙D=GF-˙GH