Metamath Proof Explorer


Theorem gsummptshft

Description: Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

Ref Expression
Hypotheses gsummptshft.b B=BaseG
gsummptshft.z 0˙=0G
gsummptshft.g φGCMnd
gsummptshft.k φK
gsummptshft.m φM
gsummptshft.n φN
gsummptshft.a φjMNAB
gsummptshft.c j=kKA=C
Assertion gsummptshft φGj=MNA=Gk=M+KN+KC

Proof

Step Hyp Ref Expression
1 gsummptshft.b B=BaseG
2 gsummptshft.z 0˙=0G
3 gsummptshft.g φGCMnd
4 gsummptshft.k φK
5 gsummptshft.m φM
6 gsummptshft.n φN
7 gsummptshft.a φjMNAB
8 gsummptshft.c j=kKA=C
9 ovexd φMNV
10 7 fmpttd φjMNA:MNB
11 eqid jMNA=jMNA
12 fzfid φMNFin
13 2 fvexi 0˙V
14 13 a1i φ0˙V
15 11 12 7 14 fsuppmptdm φfinSupp0˙jMNA
16 4 5 6 mptfzshft φkM+KN+KkK:M+KN+K1-1 ontoMN
17 1 2 3 9 10 15 16 gsumf1o φGj=MNA=GjMNAkM+KN+KkK
18 elfzelz kM+KN+Kk
19 18 zcnd kM+KN+Kk
20 4 zcnd φK
21 npcan kKk-K+K=k
22 19 20 21 syl2anr φkM+KN+Kk-K+K=k
23 simpr φkM+KN+KkM+KN+K
24 22 23 eqeltrd φkM+KN+Kk-K+KM+KN+K
25 5 6 jca φMN
26 25 adantr φkM+KN+KMN
27 18 adantl φkM+KN+Kk
28 4 adantr φkM+KN+KK
29 27 28 zsubcld φkM+KN+KkK
30 fzaddel MNkKKkKMNk-K+KM+KN+K
31 26 29 28 30 syl12anc φkM+KN+KkKMNk-K+KM+KN+K
32 24 31 mpbird φkM+KN+KkKMN
33 eqidd φkM+KN+KkK=kM+KN+KkK
34 eqidd φjMNA=jMNA
35 32 33 34 8 fmptco φjMNAkM+KN+KkK=kM+KN+KC
36 35 oveq2d φGjMNAkM+KN+KkK=Gk=M+KN+KC
37 17 36 eqtrd φGj=MNA=Gk=M+KN+KC