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	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumcom.2	$$⊢\phi \to B\in \mathrm{Fin}$$
	fsumcom.3	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in ℂ$$
Assertion	fsumcom	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}C=\sum _{k\in B}\sum _{j\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumcom.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumcom.2	$$⊢\phi \to B\in \mathrm{Fin}$$
3		fsumcom.3	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in ℂ$$
4	2	adantr	$$⊢\left(\phi \wedge j\in A\right)\to B\in \mathrm{Fin}$$
5		ancom	$$⊢\left(j\in A\wedge k\in B\right)\leftrightarrow \left(k\in B\wedge j\in A\right)$$
6	5	a1i	$$⊢\phi \to \left(\left(j\in A\wedge k\in B\right)\leftrightarrow \left(k\in B\wedge j\in A\right)\right)$$
7	1 2 4 6 3	fsumcom2	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}C=\sum _{k\in B}\sum _{j\in A}C$$