This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ 𝐶 ) ) )