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

Theorem sge0iunmptlemfi 43095
 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 4898 . . . . 5 (𝑦 = ∅ → 𝑥𝑦 𝐵 = 𝑥 ∈ ∅ 𝐵)
21mpteq1d 5120 . . . 4 (𝑦 = ∅ → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ ∅ 𝐵𝐶))
32fveq2d 6650 . . 3 (𝑦 = ∅ → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)))
4 mpteq1 5119 . . . 4 (𝑦 = ∅ → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
54fveq2d 6650 . . 3 (𝑦 = ∅ → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
63, 5eqeq12d 2814 . 2 (𝑦 = ∅ → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))))
7 iuneq1 4898 . . . . 5 (𝑦 = 𝑧 𝑥𝑦 𝐵 = 𝑥𝑧 𝐵)
87mpteq1d 5120 . . . 4 (𝑦 = 𝑧 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝑧 𝐵𝐶))
98fveq2d 6650 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)))
10 mpteq1 5119 . . . 4 (𝑦 = 𝑧 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))
1110fveq2d 6650 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
129, 11eqeq12d 2814 . 2 (𝑦 = 𝑧 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))))
13 iuneq1 4898 . . . . 5 (𝑦 = (𝑧 ∪ {𝑤}) → 𝑥𝑦 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
1413mpteq1d 5120 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶))
1514fveq2d 6650 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)))
16 mpteq1 5119 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))
1716fveq2d 6650 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
1815, 17eqeq12d 2814 . 2 (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
19 iuneq1 4898 . . . . 5 (𝑦 = 𝐴 𝑥𝑦 𝐵 = 𝑥𝐴 𝐵)
2019mpteq1d 5120 . . . 4 (𝑦 = 𝐴 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶))
2120fveq2d 6650 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
22 mpteq1 5119 . . . 4 (𝑦 = 𝐴 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
2322fveq2d 6650 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
2421, 23eqeq12d 2814 . 2 (𝑦 = 𝐴 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
25 0iun 4950 . . . . . . 7 𝑥 ∈ ∅ 𝐵 = ∅
26 mpteq1 5119 . . . . . . 7 ( 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
2725, 26ax-mp 5 . . . . . 6 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28 mpt0 6463 . . . . . 6 (𝑘 ∈ ∅ ↦ 𝐶) = ∅
2927, 28eqtri 2821 . . . . 5 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = ∅
3029fveq2i 6649 . . . 4 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘∅)
31 mpt0 6463 . . . . 5 (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))) = ∅
3231fveq2i 6649 . . . 4 ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘∅)
3330, 32eqtr4i 2824 . . 3 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
3433a1i 11 . 2 (𝜑 → (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
35 nfv 1915 . . . . . . 7 𝑥(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
36 nfcv 2955 . . . . . . . 8 𝑥Σ^
37 nfiu1 4916 . . . . . . . . 9 𝑥 𝑥 ∈ {𝑤}𝐵
38 nfcv 2955 . . . . . . . . 9 𝑥𝐶
3937, 38nfmpt 5128 . . . . . . . 8 𝑥(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)
4036, 39nffv 6656 . . . . . . 7 𝑥^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
41 simprl 770 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧𝐴)
42 sge0iunmptlemfi.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
4342adantr 484 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝐴 ∈ Fin)
44 simpr 488 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧𝐴)
45 ssfi 8725 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑧𝐴) → 𝑧 ∈ Fin)
4643, 44, 45syl2anc 587 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑧 ∈ Fin)
4741, 46syldan 594 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧 ∈ Fin)
48 simprr 772 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑤 ∈ (𝐴𝑧))
49 eldifn 4055 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → ¬ 𝑤𝑧)
50 disjsn 4607 . . . . . . . . . . 11 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5149, 50sylibr 237 . . . . . . . . . 10 (𝑤 ∈ (𝐴𝑧) → (𝑧 ∩ {𝑤}) = ∅)
5251adantl 485 . . . . . . . . 9 ((𝑧𝐴𝑤 ∈ (𝐴𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
5352adantl 485 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
5453, 50sylib 221 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ¬ 𝑤𝑧)
55 simpll 766 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝜑)
56 ssel2 3910 . . . . . . . . . . 11 ((𝑧𝐴𝑥𝑧) → 𝑥𝐴)
5756adantll 713 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝑥𝐴)
58 sge0iunmptlemfi.re . . . . . . . . . 10 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
5955, 57, 58syl2anc 587 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
6059recnd 10661 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
6160adantlrr 720 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
62 csbeq1a 3842 . . . . . . . . . 10 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
63 nfcsb1v 3852 . . . . . . . . . . 11 𝑥𝑤 / 𝑥𝐵
64 vex 3444 . . . . . . . . . . 11 𝑤 ∈ V
6563, 64, 62iunxsnf 41741 . . . . . . . . . 10 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
6662, 65eqtr4di 2851 . . . . . . . . 9 (𝑥 = 𝑤𝐵 = 𝑥 ∈ {𝑤}𝐵)
6766mpteq1d 5120 . . . . . . . 8 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
6867fveq2d 6650 . . . . . . 7 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)))
6965mpteq1i 5121 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶)
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
7170fveq2d 6650 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
72 eldifi 4054 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑤𝐴)
73 nfv 1915 . . . . . . . . . . . . 13 𝑥(𝜑𝑤𝐴)
7463, 38nfmpt 5128 . . . . . . . . . . . . . . 15 𝑥(𝑘𝑤 / 𝑥𝐵𝐶)
7536, 74nffv 6656 . . . . . . . . . . . . . 14 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶))
76 nfcv 2955 . . . . . . . . . . . . . 14 𝑥
7775, 76nfel 2969 . . . . . . . . . . . . 13 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ
7873, 77nfim 1897 . . . . . . . . . . . 12 𝑥((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
79 eleq1w 2872 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
8079anbi2d 631 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
8167, 69eqtrdi 2849 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
8281fveq2d 6650 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
8382eleq1d 2874 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ↔ (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ))
8480, 83imbi12d 348 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ) ↔ ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)))
8578, 84, 58chvarfv 2240 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8672, 85sylan2 595 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8771, 86eqeltrd 2890 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8887adantrl 715 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8988recnd 10661 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℂ)
9035, 40, 47, 48, 54, 61, 68, 89fsumsplitsn 15095 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
9190eqcomd 2804 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
9291adantr 484 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
93 iunxun 4980 . . . . . . . . . 10 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
9493mpteq1i 5121 . . . . . . . . 9 (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) = (𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
9594fveq2i 6649 . . . . . . . 8 ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
9695a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97 nfv 1915 . . . . . . . 8 𝑘(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
98 sge0iunmptlemfi.b . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵𝑉)
9998ralrimiva 3149 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
100 iunexg 7649 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑥𝐴 𝐵 ∈ V)
10142, 99, 100syl2anc 587 . . . . . . . . . . 11 (𝜑 𝑥𝐴 𝐵 ∈ V)
102101adantr 484 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝐴 𝐵 ∈ V)
103 iunss1 4896 . . . . . . . . . . 11 (𝑧𝐴 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
104103adantl 485 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
105102, 104ssexd 5193 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 ∈ V)
106105adantrr 716 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥𝑧 𝐵 ∈ V)
107101adantr 484 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥𝐴 𝐵 ∈ V)
108 snssi 4701 . . . . . . . . . . . . 13 (𝑤𝐴 → {𝑤} ⊆ 𝐴)
10972, 108syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴𝑧) → {𝑤} ⊆ 𝐴)
110 iunss1 4896 . . . . . . . . . . . 12 ({𝑤} ⊆ 𝐴 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
111109, 110syl 17 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
112111adantl 485 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
113107, 112ssexd 5193 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
114113adantrl 715 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
115 sge0iunmptlemfi.dj . . . . . . . . . 10 (𝜑Disj 𝑥𝐴 𝐵)
116115adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Disj 𝑥𝐴 𝐵)
117109ad2antll 728 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ⊆ 𝐴)
118 disjiun 5018 . . . . . . . . 9 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
119116, 41, 117, 53, 118syl13anc 1369 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
120 eliun 4886 . . . . . . . . . . . 12 (𝑘 𝑥𝑧 𝐵 ↔ ∃𝑥𝑧 𝑘𝐵)
121120biimpi 219 . . . . . . . . . . 11 (𝑘 𝑥𝑧 𝐵 → ∃𝑥𝑧 𝑘𝐵)
122121adantl 485 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → ∃𝑥𝑧 𝑘𝐵)
123 simp1l 1194 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝜑)
124573adant3 1129 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑥𝐴)
125 simp3 1135 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑘𝐵)
126 sge0iunmptlemfi.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
127123, 124, 125, 126syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1281273exp 1116 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝑥𝑧 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
129128rexlimdv 3242 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
130129adantr 484 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
131122, 130mpd 15 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132131adantlrr 720 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133 eliun 4886 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘𝐵)
134133biimpi 219 . . . . . . . . . . 11 (𝑘 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘𝐵)
135134adantl 485 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘𝐵)
136 simp1l 1194 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝜑)
137109sselda 3915 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
138137adantll 713 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
1391383adant3 1129 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑥𝐴)
140 simp3 1135 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑘𝐵)
141136, 139, 140, 126syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1421413exp 1116 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑥 ∈ {𝑤} → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
143142rexlimdv 3242 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
144143adantr 484 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
145135, 144mpd 15 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146145adantlrl 719 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
14797, 106, 114, 119, 132, 146sge0splitmpt 43093 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
14896, 147eqtrd 2833 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
149148adantr 484 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
150 id 22 . . . . . . . . 9 ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
151150adantl 485 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
1521263expa 1115 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
153 eqid 2798 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
154152, 153fmptd 6856 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
15598, 154sge0ge0 43066 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
15658, 155jca 515 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
157 elrege0 12835 . . . . . . . . . . . . 13 ((Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞) ↔ ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
158156, 157sylibr 237 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
15955, 57, 158syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
160 eqid 2798 . . . . . . . . . . 11 (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
161159, 160fmptd 6856 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))):𝑧⟶(0[,)+∞))
16246, 161sge0fsum 43069 . . . . . . . . 9 ((𝜑𝑧𝐴) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
163162adantr 484 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
164 fveq2 6646 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
165 nfcv 2955 . . . . . . . . . . . 12 𝑥𝑧
166 nfcv 2955 . . . . . . . . . . . 12 𝑦𝑧
167 nfmpt1 5129 . . . . . . . . . . . . 13 𝑥(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
168 nfcv 2955 . . . . . . . . . . . . 13 𝑥𝑦
169167, 168nffv 6656 . . . . . . . . . . . 12 𝑥((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦)
170 nfcv 2955 . . . . . . . . . . . 12 𝑦((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
171164, 165, 166, 169, 170cbvsum 15047 . . . . . . . . . . 11 Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
172171a1i 11 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
173 id 22 . . . . . . . . . . . . . 14 (𝑥𝑧𝑥𝑧)
174 fvexd 6661 . . . . . . . . . . . . . 14 (𝑥𝑧 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
175160fvmpt2 6757 . . . . . . . . . . . . . 14 ((𝑥𝑧 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
176173, 174, 175syl2anc 587 . . . . . . . . . . . . 13 (𝑥𝑧 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
177176adantl 485 . . . . . . . . . . . 12 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
178177ralrimiva 3149 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → ∀𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
179178sumeq2d 15054 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
180172, 179eqtrd 2833 . . . . . . . . 9 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
181180adantr 484 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
182151, 163, 1813eqtrd 2837 . . . . . . 7 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
183182adantlrr 720 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
184183oveq1d 7151 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
18546, 59fsumrecl 15086 . . . . . . . 8 ((𝜑𝑧𝐴) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
186185adantrr 716 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
187 rexadd 12616 . . . . . . 7 ((Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
188186, 88, 187syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
189188adantr 484 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
190149, 184, 1893eqtrd 2837 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
191 snfi 8580 . . . . . . . 8 {𝑤} ∈ Fin
192191a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ∈ Fin)
193 unfi 8772 . . . . . . 7 ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
19447, 192, 193syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
195 simpll 766 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
19656ad4ant14 751 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥𝑧) → 𝑥𝐴)
197 simpll 766 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑤 ∈ (𝐴𝑧))
198 elunnel1 4077 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 ∈ {𝑤})
199 elsni 4542 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
200198, 199syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
201200adantll 713 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
202 simpr 488 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
20372adantr 484 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑤𝐴)
204202, 203eqeltrd 2890 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥𝐴)
205197, 201, 204syl2anc 587 . . . . . . . . . 10 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
206205adantlll 717 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
207196, 206pm2.61dan 812 . . . . . . . 8 (((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
208207adantll 713 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
209195, 208, 158syl2anc 587 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
210194, 209sge0fsummpt 43072 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
211210adantr 484 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
21292, 190, 2113eqtr4d 2843 . . 3 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
213212ex 416 . 2 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
2146, 12, 18, 24, 34, 213, 42findcard2d 8747 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3441  ⦋csb 3828   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  ∪ ciun 4882  Disj wdisj 4996   class class class wbr 5031   ↦ cmpt 5111  ‘cfv 6325  (class class class)co 7136  Fincfn 8495  ℂcc 10527  ℝcr 10528  0cc0 10529   + caddc 10532  +∞cpnf 10664   ≤ cle 10668   +𝑒 cxad 12496  [,)cico 12731  [,]cicc 12732  Σcsu 15037  Σ^csumge0 43044 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-sup 8893  df-oi 8961  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-n0 11889  df-z 11973  df-uz 12235  df-rp 12381  df-xadd 12499  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-seq 13368  df-exp 13429  df-hash 13690  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038  df-sumge0 43045 This theorem is referenced by:  sge0iunmptlemre  43097
 Copyright terms: Public domain W3C validator