ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fsumiun GIF version

Theorem fsumiun 11253
Description: Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
Hypotheses
Ref Expression
fsumiun.1 (𝜑𝐴 ∈ Fin)
fsumiun.2 ((𝜑𝑥𝐴) → 𝐵 ∈ Fin)
fsumiun.3 (𝜑Disj 𝑥𝐴 𝐵)
fsumiun.4 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
Assertion
Ref Expression
fsumiun (𝜑 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
Distinct variable groups:   𝑥,𝑘,𝐴   𝐵,𝑘   𝜑,𝑘,𝑥   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)

Proof of Theorem fsumiun
Dummy variables 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3117 . 2 𝐴𝐴
2 fsumiun.1 . . 3 (𝜑𝐴 ∈ Fin)
3 sseq1 3120 . . . . . 6 (𝑢 = ∅ → (𝑢𝐴 ↔ ∅ ⊆ 𝐴))
4 iuneq1 3826 . . . . . . . . 9 (𝑢 = ∅ → 𝑥𝑢 𝐵 = 𝑥 ∈ ∅ 𝐵)
5 0iun 3870 . . . . . . . . 9 𝑥 ∈ ∅ 𝐵 = ∅
64, 5syl6eq 2188 . . . . . . . 8 (𝑢 = ∅ → 𝑥𝑢 𝐵 = ∅)
76sumeq1d 11142 . . . . . . 7 (𝑢 = ∅ → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 ∈ ∅ 𝐶)
8 sumeq1 11131 . . . . . . 7 (𝑢 = ∅ → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)
97, 8eqeq12d 2154 . . . . . 6 (𝑢 = ∅ → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
103, 9imbi12d 233 . . . . 5 (𝑢 = ∅ → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)))
1110imbi2d 229 . . . 4 (𝑢 = ∅ → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))))
12 sseq1 3120 . . . . . 6 (𝑢 = 𝑧 → (𝑢𝐴𝑧𝐴))
13 iuneq1 3826 . . . . . . . 8 (𝑢 = 𝑧 𝑥𝑢 𝐵 = 𝑥𝑧 𝐵)
1413sumeq1d 11142 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝑧 𝐵𝐶)
15 sumeq1 11131 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)
1614, 15eqeq12d 2154 . . . . . 6 (𝑢 = 𝑧 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
1712, 16imbi12d 233 . . . . 5 (𝑢 = 𝑧 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)))
1817imbi2d 229 . . . 4 (𝑢 = 𝑧 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))))
19 sseq1 3120 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (𝑢𝐴 ↔ (𝑧 ∪ {𝑤}) ⊆ 𝐴))
20 iuneq1 3826 . . . . . . . 8 (𝑢 = (𝑧 ∪ {𝑤}) → 𝑥𝑢 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
2120sumeq1d 11142 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)
22 sumeq1 11131 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)
2321, 22eqeq12d 2154 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
2419, 23imbi12d 233 . . . . 5 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
2524imbi2d 229 . . . 4 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
26 sseq1 3120 . . . . . 6 (𝑢 = 𝐴 → (𝑢𝐴𝐴𝐴))
27 iuneq1 3826 . . . . . . . 8 (𝑢 = 𝐴 𝑥𝑢 𝐵 = 𝑥𝐴 𝐵)
2827sumeq1d 11142 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝐴 𝐵𝐶)
29 sumeq1 11131 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
3028, 29eqeq12d 2154 . . . . . 6 (𝑢 = 𝐴 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
3126, 30imbi12d 233 . . . . 5 (𝑢 = 𝐴 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
3231imbi2d 229 . . . 4 (𝑢 = 𝐴 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))))
33 sum0 11164 . . . . . 6 Σ𝑘 ∈ ∅ 𝐶 = 0
34 sum0 11164 . . . . . 6 Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶 = 0
3533, 34eqtr4i 2163 . . . . 5 Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶
36352a1i 27 . . . 4 (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
37 id 19 . . . . . . . . 9 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
3837unssad 3253 . . . . . . . 8 ((𝑧 ∪ {𝑤}) ⊆ 𝐴𝑧𝐴)
3938imim1i 60 . . . . . . 7 ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
40 oveq1 5781 . . . . . . . . . 10 𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
41 nfcv 2281 . . . . . . . . . . . . . . . . 17 𝑧𝐵
42 nfcsb1v 3035 . . . . . . . . . . . . . . . . 17 𝑥𝑧 / 𝑥𝐵
43 csbeq1a 3012 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
4441, 42, 43cbviun 3850 . . . . . . . . . . . . . . . 16 𝑥 ∈ {𝑤}𝐵 = 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵
45 vex 2689 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
46 csbeq1 3006 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵)
4745, 46iunxsn 3889 . . . . . . . . . . . . . . . 16 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵
4844, 47eqtri 2160 . . . . . . . . . . . . . . 15 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
4948ineq2i 3274 . . . . . . . . . . . . . 14 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
50 fsumiun.3 . . . . . . . . . . . . . . . 16 (𝜑Disj 𝑥𝐴 𝐵)
5150ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥𝐴 𝐵)
5238adantl 275 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑧𝐴)
53 simpr 109 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
5453unssbd 3254 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → {𝑤} ⊆ 𝐴)
55 simplr 519 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ¬ 𝑤𝑧)
56 disjsn 3585 . . . . . . . . . . . . . . . 16 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5755, 56sylibr 133 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∩ {𝑤}) = ∅)
58 disjiun 3924 . . . . . . . . . . . . . . 15 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
5951, 52, 54, 57, 58syl13anc 1218 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
6049, 59syl5eqr 2186 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵) = ∅)
6160adantlrl 473 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵) = ∅)
62 iunxun 3892 . . . . . . . . . . . . . 14 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
6348uneq2i 3227 . . . . . . . . . . . . . 14 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6462, 63eqtri 2160 . . . . . . . . . . . . 13 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6564a1i 9 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵))
66 simplrl 524 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑧 ∈ Fin)
6745a1i 9 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑤 ∈ V)
6855adantlrl 473 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ¬ 𝑤𝑧)
69 unsnfi 6807 . . . . . . . . . . . . . 14 ((𝑧 ∈ Fin ∧ 𝑤 ∈ V ∧ ¬ 𝑤𝑧) → (𝑧 ∪ {𝑤}) ∈ Fin)
7066, 67, 68, 69syl3anc 1216 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ∈ Fin)
71 fsumiun.2 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵 ∈ Fin)
7271ralrimiva 2505 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴 𝐵 ∈ Fin)
7372ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 𝐵 ∈ Fin)
74 ssralv 3161 . . . . . . . . . . . . . . 15 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (∀𝑥𝐴 𝐵 ∈ Fin → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin))
7553, 73, 74sylc 62 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
7675adantlrl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
77 disjss1 3912 . . . . . . . . . . . . . . 15 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (Disj 𝑥𝐴 𝐵Disj 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵))
7853, 51, 77sylc 62 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
7978adantlrl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
80 iunfidisj 6834 . . . . . . . . . . . . 13 (((𝑧 ∪ {𝑤}) ∈ Fin ∧ ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin ∧ Disj 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
8170, 76, 79, 80syl3anc 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
82 iunss1 3824 . . . . . . . . . . . . . . 15 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
8382adantl 275 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
8483sselda 3097 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝑘 𝑥𝐴 𝐵)
85 eliun 3817 . . . . . . . . . . . . . . 15 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
86 fsumiun.4 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
8786rexlimdvaa 2550 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8887ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8985, 88syl5bi 151 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑘 𝑥𝐴 𝐵𝐶 ∈ ℂ))
9089imp 123 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ ℂ)
9184, 90syldan 280 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝐶 ∈ ℂ)
9261, 65, 81, 91fsumsplit 11183 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
9368, 56sylibr 133 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∩ {𝑤}) = ∅)
94 eqidd 2140 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) = (𝑧 ∪ {𝑤}))
95 simplr 519 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
96 simpr 109 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥 ∈ (𝑧 ∪ {𝑤}))
9795, 96sseldd 3098 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
9886anassrs 397 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
9971, 98fsumcl 11176 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
10099ralrimiva 2505 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
101100ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
102101r19.21bi 2520 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
10397, 102syldan 280 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → Σ𝑘𝐵 𝐶 ∈ ℂ)
10493, 94, 70, 103fsumsplit 11183 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶))
105 nfcv 2281 . . . . . . . . . . . . . . . 16 𝑧Σ𝑘𝐵 𝐶
106 nfcv 2281 . . . . . . . . . . . . . . . . 17 𝑥𝐶
10742, 106nfsum 11133 . . . . . . . . . . . . . . . 16 𝑥Σ𝑘 𝑧 / 𝑥𝐵𝐶
10843sumeq1d 11142 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑧 / 𝑥𝐵𝐶)
109105, 107, 108cbvsumi 11138 . . . . . . . . . . . . . . 15 Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶
11045snss 3649 . . . . . . . . . . . . . . . . . 18 (𝑤𝐴 ↔ {𝑤} ⊆ 𝐴)
11154, 110sylibr 133 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑤𝐴)
112100ad2antrr 479 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
113 nfcsb1v 3035 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑤 / 𝑥𝐵
114113, 106nfsum 11133 . . . . . . . . . . . . . . . . . . 19 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶
115114nfel1 2292 . . . . . . . . . . . . . . . . . 18 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ
116 csbeq1a 3012 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
117116sumeq1d 11142 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
118117eleq1d 2208 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (Σ𝑘𝐵 𝐶 ∈ ℂ ↔ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
119115, 118rspc 2783 . . . . . . . . . . . . . . . . 17 (𝑤𝐴 → (∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
120111, 112, 119sylc 62 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ)
12146sumeq1d 11142 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → Σ𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
122121sumsn 11187 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ V ∧ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
12345, 120, 122sylancr 410 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
124109, 123syl5eq 2184 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
125124oveq2d 5790 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
126125adantlrl 473 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
127104, 126eqtrd 2172 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
12892, 127eqeq12d 2154 . . . . . . . . . 10 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 ↔ (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶)))
12940, 128syl5ibr 155 . . . . . . . . 9 (((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
130129ex 114 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
131130a2d 26 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) → (((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
13239, 131syl5 32 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ Fin ∧ ¬ 𝑤𝑧)) → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
133132expcom 115 . . . . 5 ((𝑧 ∈ Fin ∧ ¬ 𝑤𝑧) → (𝜑 → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
134133a2d 26 . . . 4 ((𝑧 ∈ Fin ∧ ¬ 𝑤𝑧) → ((𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
13511, 18, 25, 32, 36, 134findcard2s 6784 . . 3 (𝐴 ∈ Fin → (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
1362, 135mpcom 36 . 2 (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
1371, 136mpi 15 1 (𝜑 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103   = wceq 1331  wcel 1480  wral 2416  wrex 2417  Vcvv 2686  csb 3003  cun 3069  cin 3070  wss 3071  c0 3363  {csn 3527   ciun 3813  Disj wdisj 3906  (class class class)co 5774  Fincfn 6634  cc 7625  0cc0 7627   + caddc 7630  Σcsu 11129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745  ax-arch 7746  ax-caucvg 7747
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-disj 3907  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-inn 8728  df-2 8786  df-3 8787  df-4 8788  df-n0 8985  df-z 9062  df-uz 9334  df-q 9419  df-rp 9449  df-fz 9798  df-fzo 9927  df-seqfrec 10226  df-exp 10300  df-ihash 10529  df-cj 10621  df-re 10622  df-im 10623  df-rsqrt 10777  df-abs 10778  df-clim 11055  df-sumdc 11130
This theorem is referenced by:  hashiun  11254
  Copyright terms: Public domain W3C validator