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 )