Metamath Proof Explorer

Theorem fsummulc2

Description: A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsummulc2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsummulc2.2 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
fsummulc2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsummulc2 ( 𝜑 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fsummulc2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsummulc2.2 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3 fsummulc2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 2 mul01d ⊢ ( 𝜑 → ( 𝐶 · 0 ) = 0 )
5 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
6 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
7 5 6 eqtrdi ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = 0 )
8 7 oveq2d ⊢ ( 𝐴 = ∅ → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝐶 · 0 ) )
9 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) = Σ 𝑘 ∈ ∅ ( 𝐶 · 𝐵 ) )
10 sum0 ⊢ Σ 𝑘 ∈ ∅ ( 𝐶 · 𝐵 ) = 0
11 9 10 eqtrdi ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) = 0 )
12 8 11 eqeq12d ⊢ ( 𝐴 = ∅ → ( ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ↔ ( 𝐶 · 0 ) = 0 ) )
13 4 12 syl5ibrcom ⊢ ( 𝜑 → ( 𝐴 = ∅ → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
14 addcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝑛 + 𝑚 ) ∈ ℂ )
16 2 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝐶 ∈ ℂ )
17 adddi ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
18 17 3expb ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
19 16 18 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝐶 · ( 𝑛 + 𝑚 ) ) = ( ( 𝐶 · 𝑛 ) + ( 𝐶 · 𝑚 ) ) )
20 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
21 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
22 20 21 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
23 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
25 simprr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
27 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
28 26 27 syl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
29 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
30 24 28 29 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
31 simpr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
32 30 31 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
33 28 31 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
35 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
36 35 3 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
37 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) )
38 37 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · 𝐵 ) )
39 34 36 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · 𝐵 ) )
40 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
41 40 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
42 34 3 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
43 42 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐶 · 𝐵 ) )
44 39 43 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) )
47 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) )
48 nfcv ⊢ Ⅎ 𝑘 𝐶
49 nfcv ⊢ Ⅎ 𝑘 ·
50 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) )
51 48 49 50 nfov ⊢ Ⅎ 𝑘 ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
52 47 51 nfeq ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
53 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
54 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
55 54 oveq2d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
56 53 55 eqeq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
57 52 56 rspc ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑘 ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
58 33 46 57 sylc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
59 27 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
60 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
61 59 60 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
62 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
63 59 62 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
64 63 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐶 · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ) = ( 𝐶 · ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
65 58 61 64 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐶 · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ) )
66 15 19 22 32 65 seqdistr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐶 · ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
67 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
68 36 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
70 69 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) ∈ ℂ )
71 67 20 25 70 61 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
72 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
73 23 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
74 73 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
75 72 20 25 74 63 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
76 75 oveq2d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐶 · ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
77 66 71 76 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) )
78 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐵
79 78 oveq2i ⊢ ( 𝐶 · Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 )
80 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 )
81 77 79 80 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )
82 81 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
83 82 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
84 83 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) ) )
85 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
86 1 85 syl ⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
87 13 84 86 mpjaod ⊢ ( 𝜑 → ( 𝐶 · Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐶 · 𝐵 ) )