Metamath Proof Explorer


Theorem fprod2d

Description: Write a double product as a product over a two-dimensional region. Compare fsum2d . (Contributed by Scott Fenton, 30-Jan-2018)

Ref Expression
Hypotheses fprod2d.1 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
fprod2d.2 ( 𝜑𝐴 ∈ Fin )
fprod2d.3 ( ( 𝜑𝑗𝐴 ) → 𝐵 ∈ Fin )
fprod2d.4 ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion fprod2d ( 𝜑 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 )

Proof

Step Hyp Ref Expression
1 fprod2d.1 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
2 fprod2d.2 ( 𝜑𝐴 ∈ Fin )
3 fprod2d.3 ( ( 𝜑𝑗𝐴 ) → 𝐵 ∈ Fin )
4 fprod2d.4 ( ( 𝜑 ∧ ( 𝑗𝐴𝑘𝐵 ) ) → 𝐶 ∈ ℂ )
5 ssid 𝐴𝐴
6 sseq1 ( 𝑤 = ∅ → ( 𝑤𝐴 ↔ ∅ ⊆ 𝐴 ) )
7 prodeq1 ( 𝑤 = ∅ → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 )
8 iuneq1 ( 𝑤 = ∅ → 𝑗𝑤 ( { 𝑗 } × 𝐵 ) = 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) )
9 0iun 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) = ∅
10 8 9 eqtrdi ( 𝑤 = ∅ → 𝑗𝑤 ( { 𝑗 } × 𝐵 ) = ∅ )
11 10 prodeq1d ( 𝑤 = ∅ → ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 = ∏ 𝑧 ∈ ∅ 𝐷 )
12 7 11 eqeq12d ( 𝑤 = ∅ → ( ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ↔ ∏ 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ∅ 𝐷 ) )
13 6 12 imbi12d ( 𝑤 = ∅ → ( ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ↔ ( ∅ ⊆ 𝐴 → ∏ 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ∅ 𝐷 ) ) )
14 13 imbi2d ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐴 → ∏ 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ∅ 𝐷 ) ) ) )
15 sseq1 ( 𝑤 = 𝑥 → ( 𝑤𝐴𝑥𝐴 ) )
16 prodeq1 ( 𝑤 = 𝑥 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑗𝑥𝑘𝐵 𝐶 )
17 iuneq1 ( 𝑤 = 𝑥 𝑗𝑤 ( { 𝑗 } × 𝐵 ) = 𝑗𝑥 ( { 𝑗 } × 𝐵 ) )
18 17 prodeq1d ( 𝑤 = 𝑥 → ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
19 16 18 eqeq12d ( 𝑤 = 𝑥 → ( ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ↔ ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) )
20 15 19 imbi12d ( 𝑤 = 𝑥 → ( ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ↔ ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
21 20 imbi2d ( 𝑤 = 𝑥 → ( ( 𝜑 → ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ↔ ( 𝜑 → ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
22 sseq1 ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ( 𝑤𝐴 ↔ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) )
23 prodeq1 ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 )
24 iuneq1 ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → 𝑗𝑤 ( { 𝑗 } × 𝐵 ) = 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) )
25 24 prodeq1d ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )
26 23 25 eqeq12d ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ( ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ↔ ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) )
27 22 26 imbi12d ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ( ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ↔ ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
28 27 imbi2d ( 𝑤 = ( 𝑥 ∪ { 𝑦 } ) → ( ( 𝜑 → ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ↔ ( 𝜑 → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
29 sseq1 ( 𝑤 = 𝐴 → ( 𝑤𝐴𝐴𝐴 ) )
30 prodeq1 ( 𝑤 = 𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑗𝐴𝑘𝐵 𝐶 )
31 iuneq1 ( 𝑤 = 𝐴 𝑗𝑤 ( { 𝑗 } × 𝐵 ) = 𝑗𝐴 ( { 𝑗 } × 𝐵 ) )
32 31 prodeq1d ( 𝑤 = 𝐴 → ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 )
33 30 32 eqeq12d ( 𝑤 = 𝐴 → ( ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ↔ ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 ) )
34 29 33 imbi12d ( 𝑤 = 𝐴 → ( ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ↔ ( 𝐴𝐴 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
35 34 imbi2d ( 𝑤 = 𝐴 → ( ( 𝜑 → ( 𝑤𝐴 → ∏ 𝑗𝑤𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑤 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ↔ ( 𝜑 → ( 𝐴𝐴 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
36 prod0 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = 1
37 prod0 𝑧 ∈ ∅ 𝐷 = 1
38 36 37 eqtr4i 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ∅ 𝐷
39 38 2a1i ( 𝜑 → ( ∅ ⊆ 𝐴 → ∏ 𝑗 ∈ ∅ ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 ∈ ∅ 𝐷 ) )
40 ssun1 𝑥 ⊆ ( 𝑥 ∪ { 𝑦 } )
41 sstr ( ( 𝑥 ⊆ ( 𝑥 ∪ { 𝑦 } ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) → 𝑥𝐴 )
42 40 41 mpan ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴𝑥𝐴 )
43 42 imim1i ( ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) )
44 2 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) → 𝐴 ∈ Fin )
45 3 ad4ant14 ( ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) ∧ 𝑗𝐴 ) → 𝐵 ∈ Fin )
46 4 ad4ant14 ( ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) ∧ ( 𝑗𝐴𝑘𝐵 ) ) → 𝐶 ∈ ℂ )
47 simplr ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) → ¬ 𝑦𝑥 )
48 simpr ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) → ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 )
49 biid ( ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ↔ ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
50 1 44 45 46 47 48 49 fprod2dlem ( ( ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) ∧ ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 ) ∧ ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )
51 50 exp31 ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ( ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
52 51 a2d ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) → ( ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
53 43 52 syl5 ( ( 𝜑 ∧ ¬ 𝑦𝑥 ) → ( ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
54 53 expcom ( ¬ 𝑦𝑥 → ( 𝜑 → ( ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
55 54 a2d ( ¬ 𝑦𝑥 → ( ( 𝜑 → ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
56 55 adantl ( ( 𝑥 ∈ Fin ∧ ¬ 𝑦𝑥 ) → ( ( 𝜑 → ( 𝑥𝐴 → ∏ 𝑗𝑥𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘𝐵 𝐶 = ∏ 𝑧 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 ) ) ) )
57 14 21 28 35 39 56 findcard2s ( 𝐴 ∈ Fin → ( 𝜑 → ( 𝐴𝐴 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 ) ) )
58 2 57 mpcom ( 𝜑 → ( 𝐴𝐴 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 ) )
59 5 58 mpi ( 𝜑 → ∏ 𝑗𝐴𝑘𝐵 𝐶 = ∏ 𝑧 𝑗𝐴 ( { 𝑗 } × 𝐵 ) 𝐷 )