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

Metamath Proof Explorer

Theorem fsumcom

Description: Interchange order of summation. (Contributed by NM, 15-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 fsumcom.1 ⊢ φ → A ∈ Fin
2 fsumcom.2 ⊢ φ → B ∈ Fin
3 fsumcom.3 ⊢ φ ∧ j ∈ A ∧ k ∈ B → C ∈ ℂ
4 2 adantr ⊢ φ ∧ j ∈ A → B ∈ Fin
5 ancom ⊢ j ∈ A ∧ k ∈ B ↔ k ∈ B ∧ j ∈ A
6 5 a1i ⊢ φ → j ∈ A ∧ k ∈ B ↔ k ∈ B ∧ j ∈ A
7 1 2 4 6 3 fsumcom2 ⊢ φ → ∑ j ∈ A ∑ k ∈ B C = ∑ k ∈ B ∑ j ∈ A C