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