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

Theorem fsumiun 15853
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 4017 . 2 𝐴𝐴
2 fsumiun.1 . . 3 (𝜑𝐴 ∈ Fin)
3 sseq1 4020 . . . . . 6 (𝑢 = ∅ → (𝑢𝐴 ↔ ∅ ⊆ 𝐴))
4 iuneq1 5012 . . . . . . . . 9 (𝑢 = ∅ → 𝑥𝑢 𝐵 = 𝑥 ∈ ∅ 𝐵)
5 0iun 5067 . . . . . . . . 9 𝑥 ∈ ∅ 𝐵 = ∅
64, 5eqtrdi 2790 . . . . . . . 8 (𝑢 = ∅ → 𝑥𝑢 𝐵 = ∅)
76sumeq1d 15732 . . . . . . 7 (𝑢 = ∅ → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 ∈ ∅ 𝐶)
8 sumeq1 15721 . . . . . . 7 (𝑢 = ∅ → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)
97, 8eqeq12d 2750 . . . . . 6 (𝑢 = ∅ → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
103, 9imbi12d 344 . . . . 5 (𝑢 = ∅ → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶)))
1110imbi2d 340 . . . 4 (𝑢 = ∅ → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))))
12 sseq1 4020 . . . . . 6 (𝑢 = 𝑧 → (𝑢𝐴𝑧𝐴))
13 iuneq1 5012 . . . . . . . 8 (𝑢 = 𝑧 𝑥𝑢 𝐵 = 𝑥𝑧 𝐵)
1413sumeq1d 15732 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝑧 𝐵𝐶)
15 sumeq1 15721 . . . . . . 7 (𝑢 = 𝑧 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)
1614, 15eqeq12d 2750 . . . . . 6 (𝑢 = 𝑧 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
1712, 16imbi12d 344 . . . . 5 (𝑢 = 𝑧 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)))
1817imbi2d 340 . . . 4 (𝑢 = 𝑧 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))))
19 sseq1 4020 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (𝑢𝐴 ↔ (𝑧 ∪ {𝑤}) ⊆ 𝐴))
20 iuneq1 5012 . . . . . . . 8 (𝑢 = (𝑧 ∪ {𝑤}) → 𝑥𝑢 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
2120sumeq1d 15732 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)
22 sumeq1 15721 . . . . . . 7 (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)
2321, 22eqeq12d 2750 . . . . . 6 (𝑢 = (𝑧 ∪ {𝑤}) → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
2419, 23imbi12d 344 . . . . 5 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
2524imbi2d 340 . . . 4 (𝑢 = (𝑧 ∪ {𝑤}) → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
26 sseq1 4020 . . . . . 6 (𝑢 = 𝐴 → (𝑢𝐴𝐴𝐴))
27 iuneq1 5012 . . . . . . . 8 (𝑢 = 𝐴 𝑥𝑢 𝐵 = 𝑥𝐴 𝐵)
2827sumeq1d 15732 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑘 𝑥𝐴 𝐵𝐶)
29 sumeq1 15721 . . . . . . 7 (𝑢 = 𝐴 → Σ𝑥𝑢 Σ𝑘𝐵 𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
3028, 29eqeq12d 2750 . . . . . 6 (𝑢 = 𝐴 → (Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶 ↔ Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
3126, 30imbi12d 344 . . . . 5 (𝑢 = 𝐴 → ((𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶) ↔ (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
3231imbi2d 340 . . . 4 (𝑢 = 𝐴 → ((𝜑 → (𝑢𝐴 → Σ𝑘 𝑥𝑢 𝐵𝐶 = Σ𝑥𝑢 Σ𝑘𝐵 𝐶)) ↔ (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))))
33 sum0 15753 . . . . . 6 Σ𝑘 ∈ ∅ 𝐶 = 0
34 sum0 15753 . . . . . 6 Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶 = 0
3533, 34eqtr4i 2765 . . . . 5 Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶
36352a1i 12 . . . 4 (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘𝐵 𝐶))
37 id 22 . . . . . . . . . 10 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
3837unssad 4202 . . . . . . . . 9 ((𝑧 ∪ {𝑤}) ⊆ 𝐴𝑧𝐴)
3938imim1i 63 . . . . . . . 8 ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶))
40 oveq1 7437 . . . . . . . . . . 11 𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
41 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑧𝐵
42 nfcsb1v 3932 . . . . . . . . . . . . . . . . 17 𝑥𝑧 / 𝑥𝐵
43 csbeq1a 3921 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
4441, 42, 43cbviun 5040 . . . . . . . . . . . . . . . 16 𝑥 ∈ {𝑤}𝐵 = 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵
45 vex 3481 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
46 csbeq1 3910 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵)
4745, 46iunxsn 5095 . . . . . . . . . . . . . . . 16 𝑧 ∈ {𝑤}𝑧 / 𝑥𝐵 = 𝑤 / 𝑥𝐵
4844, 47eqtri 2762 . . . . . . . . . . . . . . 15 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
4948ineq2i 4224 . . . . . . . . . . . . . 14 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
50 fsumiun.3 . . . . . . . . . . . . . . . 16 (𝜑Disj 𝑥𝐴 𝐵)
5150ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥𝐴 𝐵)
5238adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑧𝐴)
53 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ⊆ 𝐴)
5453unssbd 4203 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → {𝑤} ⊆ 𝐴)
55 simplr 769 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ¬ 𝑤𝑧)
56 disjsn 4715 . . . . . . . . . . . . . . . 16 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5755, 56sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∩ {𝑤}) = ∅)
58 disjiun 5135 . . . . . . . . . . . . . . 15 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
5951, 52, 54, 57, 58syl13anc 1371 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
6049, 59eqtr3id 2788 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵) = ∅)
61 iunxun 5098 . . . . . . . . . . . . . . 15 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
6248uneq2i 4174 . . . . . . . . . . . . . . 15 ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6361, 62eqtri 2762 . . . . . . . . . . . . . 14 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵)
6463a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵𝑤 / 𝑥𝐵))
652ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝐴 ∈ Fin)
6665, 53ssfid 9298 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ∈ Fin)
67 fsumiun.2 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵 ∈ Fin)
6867ralrimiva 3143 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐴 𝐵 ∈ Fin)
6968ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 𝐵 ∈ Fin)
70 ssralv 4063 . . . . . . . . . . . . . . 15 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (∀𝑥𝐴 𝐵 ∈ Fin → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin))
7153, 69, 70sylc 65 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
72 iunfi 9380 . . . . . . . . . . . . . 14 (((𝑧 ∪ {𝑤}) ∈ Fin ∧ ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
7366, 71, 72syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)
74 iunss1 5010 . . . . . . . . . . . . . . . 16 ((𝑧 ∪ {𝑤}) ⊆ 𝐴 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
7574adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 𝑥𝐴 𝐵)
7675sselda 3994 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝑘 𝑥𝐴 𝐵)
77 eliun 4999 . . . . . . . . . . . . . . . 16 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
78 fsumiun.4 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
7978rexlimdvaa 3153 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8079ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ ℂ))
8177, 80biimtrid 242 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑘 𝑥𝐴 𝐵𝐶 ∈ ℂ))
8281imp 406 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ ℂ)
8376, 82syldan 591 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝐶 ∈ ℂ)
8460, 64, 73, 83fsumsplit 15773 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
85 eqidd 2735 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) = (𝑧 ∪ {𝑤}))
8653sselda 3994 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
8778anassrs 467 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
8867, 87fsumcl 15765 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
8988ralrimiva 3143 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
9089ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ)
9190r19.21bi 3248 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
9286, 91syldan 591 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → Σ𝑘𝐵 𝐶 ∈ ℂ)
9357, 85, 66, 92fsumsplit 15773 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶))
9443sumeq1d 15732 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑧 / 𝑥𝐵𝐶)
95 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑧Σ𝑘𝐵 𝐶
96 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑥𝐶
9742, 96nfsum 15723 . . . . . . . . . . . . . . . 16 𝑥Σ𝑘 𝑧 / 𝑥𝐵𝐶
9894, 95, 97cbvsum 15727 . . . . . . . . . . . . . . 15 Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶
9945snss 4789 . . . . . . . . . . . . . . . . . 18 (𝑤𝐴 ↔ {𝑤} ⊆ 𝐴)
10054, 99sylibr 234 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑤𝐴)
101 nfcsb1v 3932 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑤 / 𝑥𝐵
102101, 96nfsum 15723 . . . . . . . . . . . . . . . . . . 19 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶
103102nfel1 2919 . . . . . . . . . . . . . . . . . 18 𝑥Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ
104 csbeq1a 3921 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
105104sumeq1d 15732 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑤 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
106105eleq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑤 → (Σ𝑘𝐵 𝐶 ∈ ℂ ↔ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
107103, 106rspc 3609 . . . . . . . . . . . . . . . . 17 (𝑤𝐴 → (∀𝑥𝐴 Σ𝑘𝐵 𝐶 ∈ ℂ → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ))
108100, 90, 107sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ)
10946sumeq1d 15732 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → Σ𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
110109sumsn 15778 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ V ∧ Σ𝑘 𝑤 / 𝑥𝐵𝐶 ∈ ℂ) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
11145, 108, 110sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑧 ∈ {𝑤𝑘 𝑧 / 𝑥𝐵𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
11298, 111eqtrid 2786 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶 = Σ𝑘 𝑤 / 𝑥𝐵𝐶)
113112oveq2d 7446 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑥 ∈ {𝑤𝑘𝐵 𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
11493, 113eqtrd 2774 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶))
11584, 114eqeq12d 2750 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶 ↔ (Σ𝑘 𝑥𝑧 𝐵𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶) = (Σ𝑥𝑧 Σ𝑘𝐵 𝐶 + Σ𝑘 𝑤 / 𝑥𝐵𝐶)))
11640, 115imbitrrid 246 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑤𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))
117116ex 412 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑤𝑧) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
118117a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑤𝑧) → (((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
11939, 118syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑤𝑧) → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶)))
120119expcom 413 . . . . . 6 𝑤𝑧 → (𝜑 → ((𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
121120a2d 29 . . . . 5 𝑤𝑧 → ((𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
122121adantl 481 . . . 4 ((𝑧 ∈ Fin ∧ ¬ 𝑤𝑧) → ((𝜑 → (𝑧𝐴 → Σ𝑘 𝑥𝑧 𝐵𝐶 = Σ𝑥𝑧 Σ𝑘𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘𝐵 𝐶))))
12311, 18, 25, 32, 36, 122findcard2s 9203 . . 3 (𝐴 ∈ Fin → (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)))
1242, 123mpcom 38 . 2 (𝜑 → (𝐴𝐴 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶))
1251, 124mpi 20 1 (𝜑 → Σ𝑘 𝑥𝐴 𝐵𝐶 = Σ𝑥𝐴 Σ𝑘𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1536  wcel 2105  wral 3058  wrex 3067  Vcvv 3477  csb 3907  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630   ciun 4995  Disj wdisj 5114  (class class class)co 7430  Fincfn 8983  cc 11150  0cc0 11152   + caddc 11155  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  hashiun  15854  incexc2  15870  musum  27248  breprexplema  34623  fsumiunss  45530
  Copyright terms: Public domain W3C validator