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

Metamath Proof Explorer

Theorem fsum2d

Description: Write a double sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j . (Contributed by Mario Carneiro, 27-Apr-2014)

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

Proof

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