Theorem fsum2mul

Description: Separate the nested sum of the product C ( j ) x. D ( k ) . (Contributed by NM, 13-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsum2mul.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsum2mul.2	$$⊢\phi \to B\in \mathrm{Fin}$$
	fsum2mul.3	$$⊢\left(\phi \wedge j\in A\right)\to C\in ℂ$$
	fsum2mul.4	$$⊢\left(\phi \wedge k\in B\right)\to D\in ℂ$$
Assertion	fsum2mul	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}CD=\sum _{j\in A}C\sum _{k\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		fsum2mul.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsum2mul.2	$$⊢\phi \to B\in \mathrm{Fin}$$
3		fsum2mul.3	$$⊢\left(\phi \wedge j\in A\right)\to C\in ℂ$$
4		fsum2mul.4	$$⊢\left(\phi \wedge k\in B\right)\to D\in ℂ$$
5	2 4	fsumcl	$$⊢\phi \to \sum _{k\in B}D\in ℂ$$
6	1 5 3	fsummulc1	$$⊢\phi \to \sum _{j\in A}C\sum _{k\in B}D=\sum _{j\in A}C\sum _{k\in B}D$$
7	2	adantr	$$⊢\left(\phi \wedge j\in A\right)\to B\in \mathrm{Fin}$$
8	4	adantlr	$$⊢\left(\left(\phi \wedge j\in A\right)\wedge k\in B\right)\to D\in ℂ$$
9	7 3 8	fsummulc2	$$⊢\left(\phi \wedge j\in A\right)\to C\sum _{k\in B}D=\sum _{k\in B}CD$$
10	9	sumeq2dv	$$⊢\phi \to \sum _{j\in A}C\sum _{k\in B}D=\sum _{j\in A}\sum _{k\in B}CD$$
11	6 10	eqtr2d	$$⊢\phi \to \sum _{j\in A}\sum _{k\in B}CD=\sum _{j\in A}C\sum _{k\in B}D$$