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 = ( Base ` G )
gsummptshft.z 
|- .0. = ( 0g ` G )
gsummptshft.g 
|- ( ph -> G e. CMnd )
gsummptshft.k 
|- ( ph -> K e. ZZ )
gsummptshft.m 
|- ( ph -> M e. ZZ )
gsummptshft.n 
|- ( ph -> N e. ZZ )
gsummptshft.a 
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. B )
gsummptshft.c 
|- ( j = ( k - K ) -> A = C )
Assertion gsummptshft 
|- ( ph -> ( G gsum ( j e. ( M ... N ) |-> A ) ) = ( G gsum ( k e. ( ( M + K ) ... ( N + K ) ) |-> C ) ) )

Proof

Step Hyp Ref Expression
1 gsummptshft.b 
 |-  B = ( Base ` G )
2 gsummptshft.z 
 |-  .0. = ( 0g ` G )
3 gsummptshft.g 
 |-  ( ph -> G e. CMnd )
4 gsummptshft.k 
 |-  ( ph -> K e. ZZ )
5 gsummptshft.m 
 |-  ( ph -> M e. ZZ )
6 gsummptshft.n 
 |-  ( ph -> N e. ZZ )
7 gsummptshft.a 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. B )
8 gsummptshft.c 
 |-  ( j = ( k - K ) -> A = C )
9 ovexd 
 |-  ( ph -> ( M ... N ) e. _V )
10 7 fmpttd 
 |-  ( ph -> ( j e. ( M ... N ) |-> A ) : ( M ... N ) --> B )
11 eqid 
 |-  ( j e. ( M ... N ) |-> A ) = ( j e. ( M ... N ) |-> A )
12 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
13 2 fvexi 
 |-  .0. e. _V
14 13 a1i 
 |-  ( ph -> .0. e. _V )
15 11 12 7 14 fsuppmptdm 
 |-  ( ph -> ( j e. ( M ... N ) |-> A ) finSupp .0. )
16 4 5 6 mptfzshft 
 |-  ( ph -> ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) : ( ( M + K ) ... ( N + K ) ) -1-1-onto-> ( M ... N ) )
17 1 2 3 9 10 15 16 gsumf1o 
 |-  ( ph -> ( G gsum ( j e. ( M ... N ) |-> A ) ) = ( G gsum ( ( j e. ( M ... N ) |-> A ) o. ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) ) ) )
18 elfzelz 
 |-  ( k e. ( ( M + K ) ... ( N + K ) ) -> k e. ZZ )
19 18 zcnd 
 |-  ( k e. ( ( M + K ) ... ( N + K ) ) -> k e. CC )
20 4 zcnd 
 |-  ( ph -> K e. CC )
21 npcan 
 |-  ( ( k e. CC /\ K e. CC ) -> ( ( k - K ) + K ) = k )
22 19 20 21 syl2anr 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( ( k - K ) + K ) = k )
23 simpr 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> k e. ( ( M + K ) ... ( N + K ) ) )
24 22 23 eqeltrd 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( ( k - K ) + K ) e. ( ( M + K ) ... ( N + K ) ) )
25 5 6 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
26 25 adantr 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
27 18 adantl 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> k e. ZZ )
28 4 adantr 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> K e. ZZ )
29 27 28 zsubcld 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( k - K ) e. ZZ )
30 fzaddel 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( k - K ) e. ZZ /\ K e. ZZ ) ) -> ( ( k - K ) e. ( M ... N ) <-> ( ( k - K ) + K ) e. ( ( M + K ) ... ( N + K ) ) ) )
31 26 29 28 30 syl12anc 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( ( k - K ) e. ( M ... N ) <-> ( ( k - K ) + K ) e. ( ( M + K ) ... ( N + K ) ) ) )
32 24 31 mpbird 
 |-  ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( k - K ) e. ( M ... N ) )
33 eqidd 
 |-  ( ph -> ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) = ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) )
34 eqidd 
 |-  ( ph -> ( j e. ( M ... N ) |-> A ) = ( j e. ( M ... N ) |-> A ) )
35 32 33 34 8 fmptco 
 |-  ( ph -> ( ( j e. ( M ... N ) |-> A ) o. ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) ) = ( k e. ( ( M + K ) ... ( N + K ) ) |-> C ) )
36 35 oveq2d 
 |-  ( ph -> ( G gsum ( ( j e. ( M ... N ) |-> A ) o. ( k e. ( ( M + K ) ... ( N + K ) ) |-> ( k - K ) ) ) ) = ( G gsum ( k e. ( ( M + K ) ... ( N + K ) ) |-> C ) ) )
37 17 36 eqtrd 
 |-  ( ph -> ( G gsum ( j e. ( M ... N ) |-> A ) ) = ( G gsum ( k e. ( ( M + K ) ... ( N + K ) ) |-> C ) ) )