Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0iunmptlemfi Structured version   Visualization version   GIF version

Theorem sge0iunmptlemfi 39937
Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0iunmptlemfi.a (𝜑𝐴 ∈ Fin)
sge0iunmptlemfi.b ((𝜑𝑥𝐴) → 𝐵𝑉)
sge0iunmptlemfi.dj (𝜑Disj 𝑥𝐴 𝐵)
sge0iunmptlemfi.c ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
sge0iunmptlemfi.re ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
Assertion
Ref Expression
sge0iunmptlemfi (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Distinct variable groups:   𝐴,𝑘,𝑥   𝐵,𝑘   𝑥,𝐶   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)   𝑉(𝑥,𝑘)

Proof of Theorem sge0iunmptlemfi
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iuneq1 4500 . . . . 5 (𝑦 = ∅ → 𝑥𝑦 𝐵 = 𝑥 ∈ ∅ 𝐵)
21mpteq1d 4698 . . . 4 (𝑦 = ∅ → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ ∅ 𝐵𝐶))
32fveq2d 6152 . . 3 (𝑦 = ∅ → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)))
4 mpteq1 4697 . . . 4 (𝑦 = ∅ → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
54fveq2d 6152 . . 3 (𝑦 = ∅ → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
63, 5eqeq12d 2636 . 2 (𝑦 = ∅ → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))))
7 iuneq1 4500 . . . . 5 (𝑦 = 𝑧 𝑥𝑦 𝐵 = 𝑥𝑧 𝐵)
87mpteq1d 4698 . . . 4 (𝑦 = 𝑧 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝑧 𝐵𝐶))
98fveq2d 6152 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)))
10 mpteq1 4697 . . . 4 (𝑦 = 𝑧 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))
1110fveq2d 6152 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
129, 11eqeq12d 2636 . 2 (𝑦 = 𝑧 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))))
13 iuneq1 4500 . . . . 5 (𝑦 = (𝑧 ∪ {𝑤}) → 𝑥𝑦 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
1413mpteq1d 4698 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶))
1514fveq2d 6152 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)))
16 mpteq1 4697 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))
1716fveq2d 6152 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
1815, 17eqeq12d 2636 . 2 (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
19 iuneq1 4500 . . . . 5 (𝑦 = 𝐴 𝑥𝑦 𝐵 = 𝑥𝐴 𝐵)
2019mpteq1d 4698 . . . 4 (𝑦 = 𝐴 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶))
2120fveq2d 6152 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
22 mpteq1 4697 . . . 4 (𝑦 = 𝐴 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
2322fveq2d 6152 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
2421, 23eqeq12d 2636 . 2 (𝑦 = 𝐴 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
25 0iun 4543 . . . . . . 7 𝑥 ∈ ∅ 𝐵 = ∅
26 mpteq1 4697 . . . . . . 7 ( 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
2725, 26ax-mp 5 . . . . . 6 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28 mpt0 5978 . . . . . 6 (𝑘 ∈ ∅ ↦ 𝐶) = ∅
2927, 28eqtri 2643 . . . . 5 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = ∅
3029fveq2i 6151 . . . 4 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘∅)
31 mpt0 5978 . . . . 5 (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))) = ∅
3231fveq2i 6151 . . . 4 ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘∅)
3330, 32eqtr4i 2646 . . 3 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
3433a1i 11 . 2 (𝜑 → (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
35 nfv 1840 . . . . . . 7 𝑥(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
36 nfcv 2761 . . . . . . . 8 𝑥Σ^
37 nfiu1 4516 . . . . . . . . 9 𝑥 𝑥 ∈ {𝑤}𝐵
38 nfcv 2761 . . . . . . . . 9 𝑥𝐶
3937, 38nfmpt 4706 . . . . . . . 8 𝑥(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)
4036, 39nffv 6155 . . . . . . 7 𝑥^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
41 simprl 793 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧𝐴)
42 sge0iunmptlemfi.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
4342adantr 481 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝐴 ∈ Fin)
44 simpr 477 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧𝐴)
45 ssfi 8124 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑧𝐴) → 𝑧 ∈ Fin)
4643, 44, 45syl2anc 692 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑧 ∈ Fin)
4741, 46syldan 487 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧 ∈ Fin)
48 simprr 795 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑤 ∈ (𝐴𝑧))
49 eldifn 3711 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → ¬ 𝑤𝑧)
50 disjsn 4216 . . . . . . . . . . 11 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5149, 50sylibr 224 . . . . . . . . . 10 (𝑤 ∈ (𝐴𝑧) → (𝑧 ∩ {𝑤}) = ∅)
5251adantl 482 . . . . . . . . 9 ((𝑧𝐴𝑤 ∈ (𝐴𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
5352adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
5453, 50sylib 208 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ¬ 𝑤𝑧)
55 simpll 789 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝜑)
56 ssel2 3578 . . . . . . . . . . 11 ((𝑧𝐴𝑥𝑧) → 𝑥𝐴)
5756adantll 749 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝑥𝐴)
58 sge0iunmptlemfi.re . . . . . . . . . 10 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
5955, 57, 58syl2anc 692 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
6059recnd 10012 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
6160adantlrr 756 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
62 csbeq1a 3523 . . . . . . . . . 10 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
63 nfcsb1v 3530 . . . . . . . . . . 11 𝑥𝑤 / 𝑥𝐵
64 vex 3189 . . . . . . . . . . 11 𝑤 ∈ V
6563, 64, 62iunxsnf 38718 . . . . . . . . . 10 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
6662, 65syl6eqr 2673 . . . . . . . . 9 (𝑥 = 𝑤𝐵 = 𝑥 ∈ {𝑤}𝐵)
6766mpteq1d 4698 . . . . . . . 8 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
6867fveq2d 6152 . . . . . . 7 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)))
6965mpteq1i 4699 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶)
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
7170fveq2d 6152 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
72 eldifi 3710 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑤𝐴)
73 nfv 1840 . . . . . . . . . . . . 13 𝑥(𝜑𝑤𝐴)
7463, 38nfmpt 4706 . . . . . . . . . . . . . . 15 𝑥(𝑘𝑤 / 𝑥𝐵𝐶)
7536, 74nffv 6155 . . . . . . . . . . . . . 14 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶))
76 nfcv 2761 . . . . . . . . . . . . . 14 𝑥
7775, 76nfel 2773 . . . . . . . . . . . . 13 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ
7873, 77nfim 1822 . . . . . . . . . . . 12 𝑥((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
79 eleq1 2686 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
8079anbi2d 739 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
8167, 69syl6eq 2671 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
8281fveq2d 6152 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
8382eleq1d 2683 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ↔ (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ))
8480, 83imbi12d 334 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ) ↔ ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)))
8578, 84, 58chvar 2261 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8672, 85sylan2 491 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8771, 86eqeltrd 2698 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8887adantrl 751 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8988recnd 10012 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℂ)
9035, 40, 47, 48, 54, 61, 68, 89fsumsplitsn 39206 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
9190eqcomd 2627 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
9291adantr 481 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
93 iunxun 4571 . . . . . . . . . 10 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
9493mpteq1i 4699 . . . . . . . . 9 (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) = (𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
9594fveq2i 6151 . . . . . . . 8 ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
9695a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97 nfv 1840 . . . . . . . 8 𝑘(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
98 sge0iunmptlemfi.b . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵𝑉)
9998ralrimiva 2960 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
100 iunexg 7089 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑥𝐴 𝐵 ∈ V)
10142, 99, 100syl2anc 692 . . . . . . . . . . 11 (𝜑 𝑥𝐴 𝐵 ∈ V)
102101adantr 481 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝐴 𝐵 ∈ V)
103 iunss1 4498 . . . . . . . . . . 11 (𝑧𝐴 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
104103adantl 482 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
105102, 104ssexd 4765 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 ∈ V)
106105adantrr 752 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥𝑧 𝐵 ∈ V)
107101adantr 481 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥𝐴 𝐵 ∈ V)
108 snssi 4308 . . . . . . . . . . . . 13 (𝑤𝐴 → {𝑤} ⊆ 𝐴)
10972, 108syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴𝑧) → {𝑤} ⊆ 𝐴)
110 iunss1 4498 . . . . . . . . . . . 12 ({𝑤} ⊆ 𝐴 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
111109, 110syl 17 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
112111adantl 482 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
113107, 112ssexd 4765 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
114113adantrl 751 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
115 sge0iunmptlemfi.dj . . . . . . . . . 10 (𝜑Disj 𝑥𝐴 𝐵)
116115adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Disj 𝑥𝐴 𝐵)
117109ad2antll 764 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ⊆ 𝐴)
118 disjiun 4603 . . . . . . . . 9 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
119116, 41, 117, 53, 118syl13anc 1325 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
120 eliun 4490 . . . . . . . . . . . 12 (𝑘 𝑥𝑧 𝐵 ↔ ∃𝑥𝑧 𝑘𝐵)
121120biimpi 206 . . . . . . . . . . 11 (𝑘 𝑥𝑧 𝐵 → ∃𝑥𝑧 𝑘𝐵)
122121adantl 482 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → ∃𝑥𝑧 𝑘𝐵)
123 simp1l 1083 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝜑)
124573adant3 1079 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑥𝐴)
125 simp3 1061 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑘𝐵)
126 sge0iunmptlemfi.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
127123, 124, 125, 126syl3anc 1323 . . . . . . . . . . . . 13 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1281273exp 1261 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝑥𝑧 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
129128rexlimdv 3023 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
130129adantr 481 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
131122, 130mpd 15 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132131adantlrr 756 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133 eliun 4490 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘𝐵)
134133biimpi 206 . . . . . . . . . . 11 (𝑘 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘𝐵)
135134adantl 482 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘𝐵)
136 simp1l 1083 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝜑)
137109sselda 3583 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
138137adantll 749 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
1391383adant3 1079 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑥𝐴)
140 simp3 1061 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑘𝐵)
141136, 139, 140, 126syl3anc 1323 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1421413exp 1261 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑥 ∈ {𝑤} → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
143142rexlimdv 3023 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
144143adantr 481 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
145135, 144mpd 15 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146145adantlrl 755 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
14797, 106, 114, 119, 132, 146sge0splitmpt 39935 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
14896, 147eqtrd 2655 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
149148adantr 481 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
150 id 22 . . . . . . . . 9 ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
151150adantl 482 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
1521263expa 1262 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
153 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
154152, 153fmptd 6340 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
15598, 154sge0ge0 39908 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
15658, 155jca 554 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
157 elrege0 12220 . . . . . . . . . . . . 13 ((Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞) ↔ ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
158156, 157sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
15955, 57, 158syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
160 eqid 2621 . . . . . . . . . . 11 (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
161159, 160fmptd 6340 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))):𝑧⟶(0[,)+∞))
16246, 161sge0fsum 39911 . . . . . . . . 9 ((𝜑𝑧𝐴) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
163162adantr 481 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
164 fveq2 6148 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
165 nfcv 2761 . . . . . . . . . . . 12 𝑥𝑧
166 nfcv 2761 . . . . . . . . . . . 12 𝑦𝑧
167 nfmpt1 4707 . . . . . . . . . . . . 13 𝑥(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
168 nfcv 2761 . . . . . . . . . . . . 13 𝑥𝑦
169167, 168nffv 6155 . . . . . . . . . . . 12 𝑥((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦)
170 nfcv 2761 . . . . . . . . . . . 12 𝑦((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
171164, 165, 166, 169, 170cbvsum 14359 . . . . . . . . . . 11 Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
172171a1i 11 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
173 id 22 . . . . . . . . . . . . . 14 (𝑥𝑧𝑥𝑧)
174 fvex 6158 . . . . . . . . . . . . . . 15 ^‘(𝑘𝐵𝐶)) ∈ V
175174a1i 11 . . . . . . . . . . . . . 14 (𝑥𝑧 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
176160fvmpt2 6248 . . . . . . . . . . . . . 14 ((𝑥𝑧 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
177173, 175, 176syl2anc 692 . . . . . . . . . . . . 13 (𝑥𝑧 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
178177adantl 482 . . . . . . . . . . . 12 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
179178ralrimiva 2960 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → ∀𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
180179sumeq2d 14366 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
181172, 180eqtrd 2655 . . . . . . . . 9 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
182181adantr 481 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
183151, 163, 1823eqtrd 2659 . . . . . . 7 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
184183adantlrr 756 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
185184oveq1d 6619 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
18646, 59fsumrecl 14398 . . . . . . . 8 ((𝜑𝑧𝐴) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
187186adantrr 752 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
188 rexadd 12006 . . . . . . 7 ((Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
189187, 88, 188syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
190189adantr 481 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
191149, 185, 1903eqtrd 2659 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
192 snfi 7982 . . . . . . . 8 {𝑤} ∈ Fin
193192a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ∈ Fin)
194 unfi 8171 . . . . . . 7 ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
19547, 193, 194syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
196 simpll 789 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
19756ad4ant14 1290 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥𝑧) → 𝑥𝐴)
198 simpll 789 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑤 ∈ (𝐴𝑧))
199 elunnel1 3732 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 ∈ {𝑤})
200 elsni 4165 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
201199, 200syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
202201adantll 749 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
203 simpr 477 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
20472adantr 481 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑤𝐴)
205203, 204eqeltrd 2698 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥𝐴)
206198, 202, 205syl2anc 692 . . . . . . . . . 10 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
207206adantlll 753 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
208197, 207pm2.61dan 831 . . . . . . . 8 (((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
209208adantll 749 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
210196, 209, 158syl2anc 692 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
211195, 210sge0fsummpt 39914 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
212211adantr 481 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
21392, 191, 2123eqtr4d 2665 . . 3 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
214213ex 450 . 2 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
2156, 12, 18, 24, 34, 214, 42findcard2d 8146 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  csb 3514  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  {csn 4148   ciun 4485  Disj wdisj 4583   class class class wbr 4613  cmpt 4673  cfv 5847  (class class class)co 6604  Fincfn 7899  cc 9878  cr 9879  0cc0 9880   + caddc 9883  +∞cpnf 10015  cle 10019   +𝑒 cxad 11888  [,)cico 12119  [,]cicc 12120  Σcsu 14350  Σ^csumge0 39886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-rp 11777  df-xadd 11891  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-sum 14351  df-sumge0 39887
This theorem is referenced by:  sge0iunmptlemre  39939
  Copyright terms: Public domain W3C validator