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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptshft.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptshft.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptshft.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	gsummptshft.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	gsummptshft.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	gsummptshft.a	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ 𝐵 )
	gsummptshft.c	⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐶 )
Assertion	gsummptshft	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptshft.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptshft.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummptshft.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptshft.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5		gsummptshft.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6		gsummptshft.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
7		gsummptshft.a	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ 𝐵 )
8		gsummptshft.c	⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐶 )
9		ovexd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
10	7	fmpttd	⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
11		eqid	⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) = ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 )
12		fzfid	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
13	2	fvexi	⊢ 0 ∈ V
14	13	a1i	⊢ ( 𝜑 → 0 ∈ V )
15	11 12 7 14	fsuppmptdm	⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) finSupp 0 )
16	4 5 6	mptfzshft	⊢ ( 𝜑 → ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
17	1 2 3 9 10 15 16	gsumf1o	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) = ( 𝐺 Σg ( ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ∘ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) ) ) )
18		elfzelz	⊢ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑘 ∈ ℤ )
19	18	zcnd	⊢ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑘 ∈ ℂ )
20	4	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
21		npcan	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑘 − 𝐾 ) + 𝐾 ) = 𝑘 )
22	19 20 21	syl2anr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑘 − 𝐾 ) + 𝐾 ) = 𝑘 )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
24	22 23	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑘 − 𝐾 ) + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
25	5 6	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
27	18	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → 𝑘 ∈ ℤ )
28	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → 𝐾 ∈ ℤ )
29	27 28	zsubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 𝑘 − 𝐾 ) ∈ ℤ )
30		fzaddel	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑘 − 𝐾 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝑘 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 − 𝐾 ) + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
31	26 29 28 30	syl12anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑘 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 − 𝐾 ) + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
32	24 31	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 𝑘 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) )
33		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) = ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) )
34		eqidd	⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) = ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) )
35	32 33 34 8	fmptco	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ∘ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) ) = ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ 𝐶 ) )
36	35	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ∘ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑘 − 𝐾 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ 𝐶 ) ) )
37	17 36	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ 𝐶 ) ) )