This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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