Metamath Proof Explorer

Theorem fsummulc1f

Description: Closure of a finite sum of complex numbers A ( k ) . A version of fsummulc1 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsummulc1f.ph ⊢ Ⅎ 𝑘 𝜑
fsummulclf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsummulclf.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
fsummulclf.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsummulc1f ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fsummulc1f.ph ⊢ Ⅎ 𝑘 𝜑
2 fsummulclf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fsummulclf.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 fsummulclf.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
6 nfcv ⊢ Ⅎ 𝑗 𝐴
7 nfcv ⊢ Ⅎ 𝑘 𝐴
8 nfcv ⊢ Ⅎ 𝑗 𝐵
9 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
10 5 6 7 8 9 cbvsum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
11 10 oveq1i ⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 )
12 11 a1i ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) )
13 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
14 1 13 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
15 9 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ
16 14 15 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
17 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
18 17 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
19 5 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
20 18 19 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
21 16 20 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
22 2 3 21 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) )
23 eqcom ⊢ ( 𝑘 = 𝑗 ↔ 𝑗 = 𝑘 )
24 23 imbi1i ⊢ ( ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
25 eqcom ⊢ ( 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 )
26 25 imbi2i ⊢ ( ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 ) )
27 24 26 bitri ⊢ ( ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 ) )
28 5 27 mpbi ⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 )
29 28 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
30 nfcv ⊢ Ⅎ 𝑘 ·
31 nfcv ⊢ Ⅎ 𝑘 𝐶
32 9 30 31 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 )
33 nfcv ⊢ Ⅎ 𝑗 ( 𝐵 · 𝐶 )
34 29 7 6 32 33 cbvsum ⊢ Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 )
35 34 a1i ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) )
36 12 22 35 3eqtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) )