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

Metamath Proof Explorer

Theorem fsum2mul

Description: Separate the nested sum of the product C ( j ) x. D ( k ) . (Contributed by NM, 13-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsum2mul.1 ⊢ φ → A ∈ Fin
fsum2mul.2 ⊢ φ → B ∈ Fin
fsum2mul.3 ⊢ φ ∧ j ∈ A → C ∈ ℂ
fsum2mul.4 ⊢ φ ∧ k ∈ B → D ∈ ℂ
Assertion fsum2mul ⊢ φ → ∑ j ∈ A ∑ k ∈ B C ⁢ D = ∑ j ∈ A C ⁢ ∑ k ∈ B D

Proof

Step Hyp Ref Expression
1 fsum2mul.1 ⊢ φ → A ∈ Fin
2 fsum2mul.2 ⊢ φ → B ∈ Fin
3 fsum2mul.3 ⊢ φ ∧ j ∈ A → C ∈ ℂ
4 fsum2mul.4 ⊢ φ ∧ k ∈ B → D ∈ ℂ
5 2 4 fsumcl ⊢ φ → ∑ k ∈ B D ∈ ℂ
6 1 5 3 fsummulc1 ⊢ φ → ∑ j ∈ A C ⁢ ∑ k ∈ B D = ∑ j ∈ A C ⁢ ∑ k ∈ B D
7 2 adantr ⊢ φ ∧ j ∈ A → B ∈ Fin
8 4 adantlr ⊢ φ ∧ j ∈ A ∧ k ∈ B → D ∈ ℂ
9 7 3 8 fsummulc2 ⊢ φ ∧ j ∈ A → C ⁢ ∑ k ∈ B D = ∑ k ∈ B C ⁢ D
10 9 sumeq2dv ⊢ φ → ∑ j ∈ A C ⁢ ∑ k ∈ B D = ∑ j ∈ A ∑ k ∈ B C ⁢ D
11 6 10 eqtr2d ⊢ φ → ∑ j ∈ A ∑ k ∈ B C ⁢ D = ∑ j ∈ A C ⁢ ∑ k ∈ B D