Theorem fsumxp

Description: Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsumxp.1	|- ( z = <. j , k >. -> D = C )
	fsumxp.2	|- ( ph -> A e. Fin )
	fsumxp.3	|- ( ph -> B e. Fin )
	fsumxp.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion	fsumxp	|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. ( A X. B ) D )

Proof

Step	Hyp	Ref	Expression
1		fsumxp.1	|- ( z = <. j , k >. -> D = C )
2		fsumxp.2	|- ( ph -> A e. Fin )
3		fsumxp.3	|- ( ph -> B e. Fin )
4		fsumxp.4	|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5	3	adantr	|- ( ( ph /\ j e. A ) -> B e. Fin )
6	1 2 5 4	fsum2d	|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D )
7		iunxpconst	|- U_ j e. A ( { j } X. B ) = ( A X. B )
8	7	sumeq1i	|- sum_ z e. U_ j e. A ( { j } X. B ) D = sum_ z e. ( A X. B ) D
9	6 8	eqtrdi	|- ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. ( A X. B ) D )