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

Metamath Proof Explorer

Theorem fsumshftd

Description: Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft . The proof demonstrates how this can be derived starting from from fsumshft . (Contributed by NM, 1-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 fsumshftd.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fsumshftd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fsumshftd.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fsumshftd.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fsumshftd.5 ⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑘 − 𝐾 ) ) → 𝐴 = 𝐵 )
6 csbeq1a ⊢ ( 𝑗 = 𝑤 → 𝐴 = ⦋ 𝑤 / 𝑗 ⦌ 𝐴 )
7 nfcv ⊢ Ⅎ 𝑤 𝐴
8 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝐴
9 6 7 8 cbvsum ⊢ Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴
10 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) )
11 8 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ
12 10 11 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ )
13 eleq1w ⊢ ( 𝑗 = 𝑤 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) )
14 13 anbi2d ⊢ ( 𝑗 = 𝑤 → ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) ) )
15 6 eleq1d ⊢ ( 𝑗 = 𝑤 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
16 14 15 imbi12d ⊢ ( 𝑗 = 𝑤 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ ) ) )
17 12 16 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ )
18 csbeq1 ⊢ ( 𝑤 = ( 𝑘 − 𝐾 ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 )
19 1 2 3 17 18 fsumshft ⊢ ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 )
20 ovexd ⊢ ( 𝜑 → ( 𝑘 − 𝐾 ) ∈ V )
21 20 5 csbied ⊢ ( 𝜑 → ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵 )
22 21 sumeq2sdv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
23 19 22 eqtrd ⊢ ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
24 9 23 eqtrid ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )