MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumiun Structured version   Visualization version   GIF version

Theorem fsumiun 15009
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 3910 . 2 𝐴𝐴
2 fsumiun.1 . . 3 (𝜑𝐴 ∈ Fin)
3 sseq1 3913 . . . . . 6 (𝑢 = ∅ → (𝑢𝐴 ↔ ∅ ⊆ 𝐴))
4 iuneq1 4840 . . . . . . . . 9 (𝑢 = ∅ → 𝑥𝑢 𝐵 = 𝑥 ∈ ∅ 𝐵)
5 0iun 4885 . . . . . . . . 9 𝑥 ∈ ∅ 𝐵 = ∅
64, 5syl6eq 2847 . . . . . . . 8 (𝑢 = ∅ → 𝑥𝑢 𝐵 = ∅)
76sumeq1d 14891 . . . . . . 7 (𝑢 = ∅ → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 ∈ ∅ 𝐶)
8 sumeq1 14879 . . . . . . 7 (𝑢 = ∅ → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)
97, 8eqeq12d 2810 . . . . . 6 (𝑢 = ∅ → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
103, 9imbi12d 346 . . . . 5 (𝑢 = ∅ → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)))
1110imbi2d 342 . . . 4 (𝑢 = ∅ → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))))
12 sseq1 3913 . . . . . 6 (𝑢 = 𝑧 → (𝑢𝐴𝑧𝐴))
13 iuneq1 4840 . . . . . . . 8 (𝑢 = 𝑧 𝑥𝑢 𝐵 = 𝑥𝑧 𝐵)
1413sumeq1d 14891 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝑧 𝐵𝐶)
15 sumeq1 14879 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)
1614, 15eqeq12d 2810 . . . . . 6 (𝑢 = 𝑧 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
1712, 16imbi12d 346 . . . . 5 (𝑢 = 𝑧 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)))
1817imbi2d 342 . . . 4 (𝑢 = 𝑧 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))))
19 sseq1 3913 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (𝑢𝐴 ↔ (𝑧 ∪ {𝑤}) ⊆ 𝐴))
20 iuneq1 4840 . . . . . . . 8 (𝑢 = (𝑧 ∪ {𝑤}) → 𝑥𝑢 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
2120sumeq1d 14891 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)
22 sumeq1 14879 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)
2321, 22eqeq12d 2810 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
2419, 23imbi12d 346 . . . . 5 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
2524imbi2d 342 . . . 4 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
26 sseq1 3913 . . . . . 6 (𝑢 = 𝐴 → (𝑢𝐴𝐴𝐴))
27 iuneq1 4840 . . . . . . . 8 (𝑢 = 𝐴 𝑥𝑢 𝐵 = 𝑥𝐴 𝐵)
2827sumeq1d 14891 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝐴 𝐵𝐶)
29 sumeq1 14879 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
3028, 29eqeq12d 2810 . . . . . 6 (𝑢 = 𝐴 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
3126, 30imbi12d 346 . . . . 5 (𝑢 = 𝐴 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
3231imbi2d 342 . . . 4 (𝑢 = 𝐴 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))))
33 sum0 14911 . . . . . 6 Σ𝑘 ∈ ∅ 𝐶 = 0
34 sum0 14911 . . . . . 6 Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶 = 0
3533, 34eqtr4i 2822 . . . . 5 Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶
36352a1i 12 . . . 4 (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
37 id 22 . . . . . . . . . 10 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
3837unssad 4084 . . . . . . . . 9 ((𝑧 ∪ {𝑤}) ⊆ 𝐴𝑧𝐴)
3938imim1i 63 . . . . . . . 8 ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
40 oveq1 7023 . . . . . . . . . . 11 𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
41 nfcv 2949 . . . . . . . . . . . . . . . . 17 𝑧𝐵
42 nfcsb1v 3833 . . . . . . . . . . . . . . . . 17 𝑥𝑧 / 𝑥𝐵
43 csbeq1a 3824 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
4441, 42, 43cbviun 4864 . . . . . . . . . . . . . . . 16 𝑥 ∈ {𝑤}𝐵 = 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵
45 vex 3440 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
46 csbeq1 3814 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵)
4745, 46iunxsn 4912 . . . . . . . . . . . . . . . 16 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵
4844, 47eqtri 2819 . . . . . . . . . . . . . . 15 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
4948ineq2i 4106 . . . . . . . . . . . . . 14 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
50 fsumiun.3 . . . . . . . . . . . . . . . 16 (𝜑Disj 𝑥𝐴 𝐵)
5150ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥𝐴 𝐵)
5238adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑧𝐴)
53 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
5453unssbd 4085 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → {𝑤} ⊆ 𝐴)
55 simplr 765 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ¬ 𝑤𝑧)
56 disjsn 4554 . . . . . . . . . . . . . . . 16 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5755, 56sylibr 235 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∩ {𝑤}) = ∅)
58 disjiun 4950 . . . . . . . . . . . . . . 15 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
5951, 52, 54, 57, 58syl13anc 1365 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
6049, 59syl5eqr 2845 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵) = ∅)
61 iunxun 4915 . . . . . . . . . . . . . . 15 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
6248uneq2i 4057 . . . . . . . . . . . . . . 15 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6361, 62eqtri 2819 . . . . . . . . . . . . . 14 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6463a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵))
652ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝐴 ∈ Fin)
6665, 53ssfid 8587 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ∈ Fin)
67 fsumiun.2 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵 ∈ Fin)
6867ralrimiva 3149 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴 𝐵 ∈ Fin)
6968ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 𝐵 ∈ Fin)
70 ssralv 3954 . . . . . . . . . . . . . . 15 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (∀𝑥𝐴 𝐵 ∈ Fin → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin))
7153, 69, 70sylc 65 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
72 iunfi 8658 . . . . . . . . . . . . . 14 (((𝑧 ∪ {𝑤}) ∈ Fin ∧ ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
7366, 71, 72syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
74 iunss1 4838 . . . . . . . . . . . . . . . 16 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
7574adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
7675sselda 3889 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝑘 𝑥𝐴 𝐵)
77 eliun 4829 . . . . . . . . . . . . . . . 16 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
78 fsumiun.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
7978rexlimdvaa 3248 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8079ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8177, 80syl5bi 243 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑘 𝑥𝐴 𝐵𝐶 ∈ ℂ))
8281imp 407 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ ℂ)
8376, 82syldan 591 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝐶 ∈ ℂ)
8460, 64, 73, 83fsumsplit 14930 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
85 eqidd 2796 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) = (𝑧 ∪ {𝑤}))
8653sselda 3889 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
8778anassrs 468 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
8867, 87fsumcl 14923 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
8988ralrimiva 3149 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
9089ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
9190r19.21bi 3175 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
9286, 91syldan 591 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → Σ𝑘𝐵 𝐶 ∈ ℂ)
9357, 85, 66, 92fsumsplit 14930 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶))
94 nfcv 2949 . . . . . . . . . . . . . . . 16 𝑧Σ𝑘𝐵 𝐶
95 nfcv 2949 . . . . . . . . . . . . . . . . 17 𝑥𝐶
9642, 95nfsum 14881 . . . . . . . . . . . . . . . 16 𝑥Σ𝑘 𝑧 / 𝑥𝐵𝐶
9743sumeq1d 14891 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑧 / 𝑥𝐵𝐶)
9894, 96, 97cbvsumi 14887 . . . . . . . . . . . . . . 15 Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶
9945snss 4625 . . . . . . . . . . . . . . . . . 18 (𝑤𝐴 ↔ {𝑤} ⊆ 𝐴)
10054, 99sylibr 235 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑤𝐴)
101 nfcsb1v 3833 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑤 / 𝑥𝐵
102101, 95nfsum 14881 . . . . . . . . . . . . . . . . . . 19 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶
103102nfel1 2963 . . . . . . . . . . . . . . . . . 18 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ
104 csbeq1a 3824 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
105104sumeq1d 14891 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
106105eleq1d 2867 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (Σ𝑘𝐵 𝐶 ∈ ℂ ↔ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
107103, 106rspc 3553 . . . . . . . . . . . . . . . . 17 (𝑤𝐴 → (∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
108100, 90, 107sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ)
10946sumeq1d 14891 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → Σ𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
110109sumsn 14934 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ V ∧ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
11145, 108, 110sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
11298, 111syl5eq 2843 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
113112oveq2d 7032 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
11493, 113eqtrd 2831 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
11584, 114eqeq12d 2810 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 ↔ (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶)))
11640, 115syl5ibr 247 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
117116ex 413 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑤𝑧) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
118117a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑤𝑧) → (((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
11939, 118syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑤𝑧) → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
120119expcom 414 . . . . . 6 𝑤𝑧 → (𝜑 → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
121120a2d 29 . . . . 5 𝑤𝑧 → ((𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
122121adantl 482 . . . 4 ((𝑧 ∈ Fin ∧ ¬ 𝑤𝑧) → ((𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
12311, 18, 25, 32, 36, 122findcard2s 8605 . . 3 (𝐴 ∈ Fin → (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
1242, 123mpcom 38 . 2 (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
1251, 124mpi 20 1 (𝜑 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1522  wcel 2081  wral 3105  wrex 3106  Vcvv 3437  csb 3811  cun 3857  cin 3858  wss 3859  c0 4211  {csn 4472   ciun 4825  Disj wdisj 4930  (class class class)co 7016  Fincfn 8357  cc 10381  0cc0 10383   + caddc 10386  Σcsu 14876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-disj 4931  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-sup 8752  df-oi 8820  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-rp 12240  df-fz 12743  df-fzo 12884  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-sum 14877
This theorem is referenced by:  hashiun  15010  incexc2  15026  musum  25450  breprexplema  31518  fsumiunss  41398
  Copyright terms: Public domain W3C validator