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

Metamath Proof Explorer

Theorem fprodxp

Description: Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018)

Ref Expression
Hypotheses fprodxp.1 
|- ( z = <. j , k >. -> D = C )
fprodxp.2 
|- ( ph -> A e. Fin )
fprodxp.3 
|- ( ph -> B e. Fin )
fprodxp.4 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion fprodxp 
|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. ( A X. B ) D )

Proof

Step Hyp Ref Expression
1 fprodxp.1 
 |-  ( z = <. j , k >. -> D = C )
2 fprodxp.2 
 |-  ( ph -> A e. Fin )
3 fprodxp.3 
 |-  ( ph -> B e. Fin )
4 fprodxp.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 fprod2d 
 |-  ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D )
7 iunxpconst 
 |-  U_ j e. A ( { j } X. B ) = ( A X. B )
8 7 prodeq1i 
 |-  prod_ z e. U_ j e. A ( { j } X. B ) D = prod_ z e. ( A X. B ) D
9 6 8 eqtrdi 
 |-  ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. ( A X. B ) D )