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 φ A Fin
fprodxp.3 φ B Fin
fprodxp.4 φ j A k B C
Assertion fprodxp φ j A k B C = z A × B D

Proof

Step Hyp Ref Expression
1 fprodxp.1 z = j k D = C
2 fprodxp.2 φ A Fin
3 fprodxp.3 φ B Fin
4 fprodxp.4 φ j A k B C
5 3 adantr φ j A B Fin
6 1 2 5 4 fprod2d φ j A k B C = z j A j × B D
7 iunxpconst j A j × B = A × B
8 7 prodeq1i z j A j × B D = z A × B D
9 6 8 eqtrdi φ j A k B C = z A × B D