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 )