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

Proof

Step	Hyp	Ref	Expression
1		fsumxp.1	$$⊢z=⟨j,k⟩\to D=C$$
2		fsumxp.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumxp.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4		fsumxp.4	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in B\right)\right)\to C\in ℂ$$
5	3	adantr	$$⊢\left(\phi \wedge j\in A\right)\to B\in \mathrm{Fin}$$
6	1 2 5 4	fsum2d	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}C=\sum _{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}D$$
7		iunxpconst	$$⊢\bigcup _{j\in A}\left(\left\{j\right\}\times B\right)=A\times B$$
8	7	sumeq1i	$$⊢\sum _{z\in \bigcup _{j\in A}\left(\left\{j\right\}\times B\right)}D=\sum _{z\in A\times B}D$$
9	6 8	eqtrdi	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}C=\sum _{z\in A\times B}D$$