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	⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
	fprodxp.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodxp.3	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	fprodxp.4	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion	fprodxp	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fprodxp.1	⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
2		fprodxp.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodxp.3	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		fprodxp.4	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
6	1 2 5 4	fprod2d	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 )
7		iunxpconst	⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ( 𝐴 × 𝐵 )
8	7	prodeq1i	⊢ ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 = ∏ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷
9	6 8	eqtrdi	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷 )