Metamath Proof Explorer


Theorem gsumzres

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

Ref Expression
Hypotheses gsumzcl.b B=BaseG
gsumzcl.0 0˙=0G
gsumzcl.z Z=CntzG
gsumzcl.g φGMnd
gsumzcl.a φAV
gsumzcl.f φF:AB
gsumzcl.c φranFZranF
gsumzres.s φFsupp0˙W
gsumzres.w φfinSupp0˙F
Assertion gsumzres φGFW=GF

Proof

Step Hyp Ref Expression
1 gsumzcl.b B=BaseG
2 gsumzcl.0 0˙=0G
3 gsumzcl.z Z=CntzG
4 gsumzcl.g φGMnd
5 gsumzcl.a φAV
6 gsumzcl.f φF:AB
7 gsumzcl.c φranFZranF
8 gsumzres.s φFsupp0˙W
9 gsumzres.w φfinSupp0˙F
10 inex1g AVAWV
11 5 10 syl φAWV
12 2 gsumz GMndAWVGkAW0˙=0˙
13 4 11 12 syl2anc φGkAW0˙=0˙
14 2 gsumz GMndAVGkA0˙=0˙
15 4 5 14 syl2anc φGkA0˙=0˙
16 13 15 eqtr4d φGkAW0˙=GkA0˙
17 16 adantr φFsupp0˙=GkAW0˙=GkA0˙
18 resres FAW=FAW
19 ffn F:ABFFnA
20 fnresdm FFnAFA=F
21 6 19 20 3syl φFA=F
22 21 reseq1d φFAW=FW
23 18 22 eqtr3id φFAW=FW
24 23 adantr φFsupp0˙=FAW=FW
25 2 fvexi 0˙V
26 25 a1i φ0˙V
27 ssid Fsupp0˙Fsupp0˙
28 27 a1i φFsupp0˙Fsupp0˙
29 6 5 26 28 gsumcllem φFsupp0˙=F=kA0˙
30 29 reseq1d φFsupp0˙=FAW=kA0˙AW
31 inss1 AWA
32 resmpt AWAkA0˙AW=kAW0˙
33 31 32 ax-mp kA0˙AW=kAW0˙
34 30 33 eqtrdi φFsupp0˙=FAW=kAW0˙
35 24 34 eqtr3d φFsupp0˙=FW=kAW0˙
36 35 oveq2d φFsupp0˙=GFW=GkAW0˙
37 29 oveq2d φFsupp0˙=GF=GkA0˙
38 17 36 37 3eqtr4d φFsupp0˙=GFW=GF
39 38 ex φFsupp0˙=GFW=GF
40 f1ofo f:1Fsupp0˙1-1 ontoFsupp0˙f:1Fsupp0˙ontoFsupp0˙
41 forn f:1Fsupp0˙ontoFsupp0˙ranf=Fsupp0˙
42 40 41 syl f:1Fsupp0˙1-1 ontoFsupp0˙ranf=Fsupp0˙
43 42 ad2antll φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙ranf=Fsupp0˙
44 8 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙Fsupp0˙W
45 43 44 eqsstrd φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙ranfW
46 cores ranfWFWf=Ff
47 45 46 syl φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙FWf=Ff
48 47 seqeq3d φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙seq1+GFWf=seq1+GFf
49 48 fveq1d φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙seq1+GFWfFsupp0˙=seq1+GFfFsupp0˙
50 eqid +G=+G
51 4 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙GMnd
52 11 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙AWV
53 6 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙F:AB
54 fssres F:ABAWAFAW:AWB
55 53 31 54 sylancl φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙FAW:AWB
56 23 feq1d φFAW:AWBFW:AWB
57 56 biimpa φFAW:AWBFW:AWB
58 55 57 syldan φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙FW:AWB
59 resss FWF
60 59 rnssi ranFWranF
61 3 cntzidss ranFZranFranFWranFranFWZranFW
62 7 60 61 sylancl φranFWZranFW
63 62 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙ranFWZranFW
64 simprl φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙Fsupp0˙
65 f1of1 f:1Fsupp0˙1-1 ontoFsupp0˙f:1Fsupp0˙1-1Fsupp0˙
66 65 ad2antll φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙f:1Fsupp0˙1-1Fsupp0˙
67 suppssdm Fsupp0˙domF
68 67 6 fssdm φFsupp0˙A
69 68 8 ssind φFsupp0˙AW
70 69 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙Fsupp0˙AW
71 f1ss f:1Fsupp0˙1-1Fsupp0˙Fsupp0˙AWf:1Fsupp0˙1-1AW
72 66 70 71 syl2anc φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙f:1Fsupp0˙1-1AW
73 6 5 fexd φFV
74 ressuppss FV0˙VFWsupp0˙Fsupp0˙
75 73 25 74 sylancl φFWsupp0˙Fsupp0˙
76 sseq2 ranf=Fsupp0˙FWsupp0˙ranfFWsupp0˙Fsupp0˙
77 75 76 syl5ibr ranf=Fsupp0˙φFWsupp0˙ranf
78 40 41 77 3syl f:1Fsupp0˙1-1 ontoFsupp0˙φFWsupp0˙ranf
79 78 adantl Fsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙φFWsupp0˙ranf
80 79 impcom φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙FWsupp0˙ranf
81 eqid FWfsupp0˙=FWfsupp0˙
82 1 2 50 3 51 52 58 63 64 72 80 81 gsumval3 φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙GFW=seq1+GFWfFsupp0˙
83 5 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙AV
84 7 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙ranFZranF
85 68 adantr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙Fsupp0˙A
86 f1ss f:1Fsupp0˙1-1Fsupp0˙Fsupp0˙Af:1Fsupp0˙1-1A
87 66 85 86 syl2anc φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙f:1Fsupp0˙1-1A
88 27 43 sseqtrrid φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙Fsupp0˙ranf
89 eqid Ffsupp0˙=Ffsupp0˙
90 1 2 50 3 51 83 53 84 64 87 88 89 gsumval3 φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙GF=seq1+GFfFsupp0˙
91 49 82 90 3eqtr4d φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙GFW=GF
92 91 expr φFsupp0˙f:1Fsupp0˙1-1 ontoFsupp0˙GFW=GF
93 92 exlimdv φFsupp0˙ff:1Fsupp0˙1-1 ontoFsupp0˙GFW=GF
94 93 expimpd φFsupp0˙ff:1Fsupp0˙1-1 ontoFsupp0˙GFW=GF
95 fsuppimp finSupp0˙FFunFFsupp0˙Fin
96 95 simprd finSupp0˙FFsupp0˙Fin
97 fz1f1o Fsupp0˙FinFsupp0˙=Fsupp0˙ff:1Fsupp0˙1-1 ontoFsupp0˙
98 9 96 97 3syl φFsupp0˙=Fsupp0˙ff:1Fsupp0˙1-1 ontoFsupp0˙
99 39 94 98 mpjaod φGFW=GF