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

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

Proof

Step Hyp Ref Expression
1 fsumxp.1 
 |-  ( z = <. j , k >. -> D = C )
2 fsumxp.2 
 |-  ( ph -> A e. Fin )
3 fsumxp.3 
 |-  ( ph -> B e. Fin )
4 fsumxp.4 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5 3 adantr 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
6 1 2 5 4 fsum2d 
 |-  ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. U_ j e. A ( { j } X. B ) D )
7 iunxpconst 
 |-  U_ j e. A ( { j } X. B ) = ( A X. B )
8 7 sumeq1i 
 |-  sum_ z e. U_ j e. A ( { j } X. B ) D = sum_ z e. ( A X. B ) D
9 6 8 eqtrdi 
 |-  ( ph -> sum_ j e. A sum_ k e. B C = sum_ z e. ( A X. B ) D )