This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )