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 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
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 ( 𝜑 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ( 𝐴 × 𝐵 ) 𝐷 )