Metamath Proof Explorer


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 φ A Fin
fsumxp.3 φ B Fin
fsumxp.4 φ j A k B C
Assertion fsumxp φ j A k B C = z A × B D

Proof

Step Hyp Ref Expression
1 fsumxp.1 z = j k D = C
2 fsumxp.2 φ A Fin
3 fsumxp.3 φ B Fin
4 fsumxp.4 φ j A k B C
5 3 adantr φ j A B Fin
6 1 2 5 4 fsum2d φ j A k B C = z j A j × B D
7 iunxpconst j A j × B = A × B
8 7 sumeq1i z j A j × B D = z A × B D
9 6 8 eqtrdi φ j A k B C = z A × B D