Metamath Proof Explorer


Theorem gsumres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

Ref Expression
Hypotheses gsumcl.b B=BaseG
gsumcl.z 0˙=0G
gsumcl.g φGCMnd
gsumcl.a φAV
gsumcl.f φF:AB
gsumres.s φFsupp0˙W
gsumres.w φfinSupp0˙F
Assertion gsumres φGFW=GF

Proof

Step Hyp Ref Expression
1 gsumcl.b B=BaseG
2 gsumcl.z 0˙=0G
3 gsumcl.g φGCMnd
4 gsumcl.a φAV
5 gsumcl.f φF:AB
6 gsumres.s φFsupp0˙W
7 gsumres.w φfinSupp0˙F
8 eqid CntzG=CntzG
9 cmnmnd GCMndGMnd
10 3 9 syl φGMnd
11 1 8 3 5 cntzcmnf φranFCntzGranF
12 1 2 8 10 4 5 11 6 7 gsumzres φGFW=GF