Step | Hyp | Ref
| Expression |
1 | | ssun1 3290 |
. . . . 5
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
2 | | fsumsplit.2 |
. . . . 5
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
3 | 1, 2 | sseqtrrid 3198 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
4 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
5 | 4 | orcd 728 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐴)) |
6 | | fsumsplit.1 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
7 | | disjel 3469 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
8 | 7 | ex 114 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
9 | 8 | con2d 619 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴)) |
10 | 9 | imp 123 |
. . . . . . . . . 10
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐴) |
11 | 6, 10 | sylan 281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐴) |
12 | 11 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐴) |
13 | 12 | olcd 729 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐴)) |
14 | 2 | eleq2d 2240 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵))) |
15 | 14 | biimpa 294 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (𝐴 ∪ 𝐵)) |
16 | | elun 3268 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
17 | 15, 16 | sylib 121 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
18 | 5, 13, 17 | mpjaodan 793 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐴)) |
19 | | df-dc 830 |
. . . . . 6
⊢
(DECID 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐴)) |
20 | 18, 19 | sylibr 133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → DECID 𝑥 ∈ 𝐴) |
21 | 20 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑈 DECID 𝑥 ∈ 𝐴) |
22 | 3 | sselda 3147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑈) |
23 | | fsumsplit.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ) |
24 | 22, 23 | syldan 280 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
25 | 24 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
26 | | fsumsplit.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ Fin) |
27 | 26 | olcd 729 |
. . . 4
⊢ (𝜑 → ((0 ∈ ℤ ∧
𝑈 ⊆
(ℤ≥‘0) ∧ ∀𝑥 ∈
(ℤ≥‘0)DECID 𝑥 ∈ 𝑈) ∨ 𝑈 ∈ Fin)) |
28 | 3, 21, 25, 27 | isumss2 11356 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0)) |
29 | | ssun2 3291 |
. . . . 5
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
30 | 29, 2 | sseqtrrid 3198 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
31 | 6 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐴) → (𝐴 ∩ 𝐵) = ∅) |
32 | 31, 7 | sylancom 418 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
33 | 32 | olcd 729 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐵)) |
34 | 17 | orcanai 923 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
35 | 34 | orcd 728 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐵)) |
36 | 33, 35, 18 | mpjaodan 793 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐵)) |
37 | | df-dc 830 |
. . . . . 6
⊢
(DECID 𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐵 ∨ ¬ 𝑥 ∈ 𝐵)) |
38 | 36, 37 | sylibr 133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → DECID 𝑥 ∈ 𝐵) |
39 | 38 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑈 DECID 𝑥 ∈ 𝐵) |
40 | 30 | sselda 3147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝑈) |
41 | 40, 23 | syldan 280 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
42 | 41 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
43 | 30, 39, 42, 27 | isumss2 11356 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0)) |
44 | 28, 43 | oveq12d 5871 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))) |
45 | | 0cnd 7913 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 0 ∈ ℂ) |
46 | | eleq1w 2231 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑥 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) |
47 | 46 | dcbid 833 |
. . . . 5
⊢ (𝑥 = 𝑘 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴)) |
48 | 21 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ∀𝑥 ∈ 𝑈 DECID 𝑥 ∈ 𝐴) |
49 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈) |
50 | 47, 48, 49 | rspcdva 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → DECID 𝑘 ∈ 𝐴) |
51 | 23, 45, 50 | ifcldcd 3561 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) |
52 | | eleq1w 2231 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑥 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵)) |
53 | 52 | dcbid 833 |
. . . . 5
⊢ (𝑥 = 𝑘 → (DECID 𝑥 ∈ 𝐵 ↔ DECID 𝑘 ∈ 𝐵)) |
54 | 39 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ∀𝑥 ∈ 𝑈 DECID 𝑥 ∈ 𝐵) |
55 | 53, 54, 49 | rspcdva 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → DECID 𝑘 ∈ 𝐵) |
56 | 23, 45, 55 | ifcldcd 3561 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) |
57 | 26, 51, 56 | fsumadd 11369 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑈 if(𝑘 ∈ 𝐵, 𝐶, 0))) |
58 | 2 | eleq2d 2240 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵))) |
59 | | elun 3268 |
. . . . . 6
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
60 | 58, 59 | bitrdi 195 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝑈 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))) |
61 | 60 | biimpa 294 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) |
62 | | iftrue 3531 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) |
63 | 62 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) |
64 | | noel 3418 |
. . . . . . . . . . 11
⊢ ¬
𝑘 ∈
∅ |
65 | 6 | eleq2d 2240 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ 𝑘 ∈ ∅)) |
66 | | elin 3310 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) |
67 | 65, 66 | bitr3di 194 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ ∅ ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) |
68 | 64, 67 | mtbii 669 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) |
69 | | imnan 685 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵) ↔ ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) |
70 | 68, 69 | sylibr 133 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵)) |
71 | 70 | imp 123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) |
72 | 71 | iffalsed 3536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 0) |
73 | 63, 72 | oveq12d 5871 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (𝐶 + 0)) |
74 | 24 | addid1d 8068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 + 0) = 𝐶) |
75 | 73, 74 | eqtrd 2203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
76 | 70 | con2d 619 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴)) |
77 | 76 | imp 123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ¬ 𝑘 ∈ 𝐴) |
78 | 77 | iffalsed 3536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0) |
79 | | iftrue 3531 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) |
80 | 79 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) |
81 | 78, 80 | oveq12d 5871 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (0 + 𝐶)) |
82 | 41 | addid2d 8069 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (0 + 𝐶) = 𝐶) |
83 | 81, 82 | eqtrd 2203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
84 | 75, 83 | jaodan 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
85 | 61, 84 | syldan 280 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = 𝐶) |
86 | 85 | sumeq2dv 11331 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = Σ𝑘 ∈ 𝑈 𝐶) |
87 | 44, 57, 86 | 3eqtr2rd 2210 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |