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