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

Metamath Proof Explorer

Theorem fsumshft

Description: Index shift of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014) (Proof shortened by AV, 8-Sep-2019)

Ref Expression
Hypotheses fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumshft.5 ⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐵 )
Assertion fsumshft ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fsumshft.5 ⊢ ( 𝑗 = ( 𝑘 − 𝐾 ) → 𝐴 = 𝐵 )
6 fzfid ⊢ ( 𝜑 → ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∈ Fin )
7 1 2 3 mptfzshft ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
8 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 − 𝐾 ) = ( 𝑘 − 𝐾 ) )
9 eqid ⊢ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) = ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) )
10 ovex ⊢ ( 𝑘 − 𝐾 ) ∈ V
11 8 9 10 fvmpt ⊢ ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) ‘ 𝑘 ) = ( 𝑘 − 𝐾 ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) ‘ 𝑘 ) = ( 𝑘 − 𝐾 ) )
13 5 6 7 12 4 fsumf1o ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )