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	|- ( ph -> A e. Fin )
	fsumcom.2	|- ( ph -> B e. Fin )
	fsumcom.3	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion	fsumcom	|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ k e. B sum_ j e. A C )

Proof

Step	Hyp	Ref	Expression
1		fsumcom.1	|- ( ph -> A e. Fin )
2		fsumcom.2	|- ( ph -> B e. Fin )
3		fsumcom.3	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
4	2	adantr	|- ( ( ph /\ j e. A ) -> B e. Fin )
5		ancom	|- ( ( j e. A /\ k e. B ) <-> ( k e. B /\ j e. A ) )
6	5	a1i	|- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. B /\ j e. A ) ) )
7	1 2 4 6 3	fsumcom2	|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ k e. B sum_ j e. A C )