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

Proof

Step	Hyp	Ref	Expression
1		fsum2mul.1	|- ( ph -> A e. Fin )
2		fsum2mul.2	|- ( ph -> B e. Fin )
3		fsum2mul.3	|- ( ( ph /\ j e. A ) -> C e. CC )
4		fsum2mul.4	|- ( ( ph /\ k e. B ) -> D e. CC )
5	2 4	fsumcl	|- ( ph -> sum_ k e. B D e. CC )
6	1 5 3	fsummulc1	|- ( ph -> ( sum_ j e. A C x. sum_ k e. B D ) = sum_ j e. A ( C x. sum_ k e. B D ) )
7	2	adantr	|- ( ( ph /\ j e. A ) -> B e. Fin )
8	4	adantlr	|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> D e. CC )
9	7 3 8	fsummulc2	|- ( ( ph /\ j e. A ) -> ( C x. sum_ k e. B D ) = sum_ k e. B ( C x. D ) )
10	9	sumeq2dv	|- ( ph -> sum_ j e. A ( C x. sum_ k e. B D ) = sum_ j e. A sum_ k e. B ( C x. D ) )
11	6 10	eqtr2d	|- ( ph -> sum_ j e. A sum_ k e. B ( C x. D ) = ( sum_ j e. A C x. sum_ k e. B D ) )