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 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
8 5 6 7 cbvsum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
9 8 oveq1i ⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 )
10 9 a1i ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) )
11 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
12 1 11 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
13 7 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ
14 12 13 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
15 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
16 15 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
17 5 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
18 16 17 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
19 14 18 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
20 2 3 19 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) )
21 eqcom ⊢ ( 𝑘 = 𝑗 ↔ 𝑗 = 𝑘 )
22 21 imbi1i ⊢ ( ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
23 eqcom ⊢ ( 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 )
24 23 imbi2i ⊢ ( ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 ) )
25 22 24 bitri ⊢ ( ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 ) )
26 5 25 mpbi ⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 )
27 26 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
28 nfcv ⊢ Ⅎ 𝑘 ·
29 nfcv ⊢ Ⅎ 𝑘 𝐶
30 7 28 29 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 )
31 nfcv ⊢ Ⅎ 𝑗 ( 𝐵 · 𝐶 )
32 27 30 31 cbvsum ⊢ Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 )
33 32 a1i ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) )
34 10 20 33 3eqtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 · 𝐶 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) )