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

Metamath Proof Explorer

Theorem fsummulc1

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

Ref Expression
Hypotheses fsummulc2.1 ⊢ φ → A ∈ Fin
fsummulc2.2 ⊢ φ → C ∈ ℂ
fsummulc2.3 ⊢ φ ∧ k ∈ A → B ∈ ℂ
Assertion fsummulc1 ⊢ φ → ∑ k ∈ A B ⁢ C = ∑ k ∈ A B ⁢ C

Proof

Step Hyp Ref Expression
1 fsummulc2.1 ⊢ φ → A ∈ Fin
2 fsummulc2.2 ⊢ φ → C ∈ ℂ
3 fsummulc2.3 ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 1 2 3 fsummulc2 ⊢ φ → C ⁢ ∑ k ∈ A B = ∑ k ∈ A C ⁢ B
5 1 3 fsumcl ⊢ φ → ∑ k ∈ A B ∈ ℂ
6 5 2 mulcomd ⊢ φ → ∑ k ∈ A B ⁢ C = C ⁢ ∑ k ∈ A B
7 2 adantr ⊢ φ ∧ k ∈ A → C ∈ ℂ
8 3 7 mulcomd ⊢ φ ∧ k ∈ A → B ⁢ C = C ⁢ B
9 8 sumeq2dv ⊢ φ → ∑ k ∈ A B ⁢ C = ∑ k ∈ A C ⁢ B
10 4 6 9 3eqtr4d ⊢ φ → ∑ k ∈ A B ⁢ C = ∑ k ∈ A B ⁢ C