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 46428
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 5008 . . . . 5 (𝑦 = ∅ → 𝑥𝑦 𝐵 = 𝑥 ∈ ∅ 𝐵)
21mpteq1d 5237 . . . 4 (𝑦 = ∅ → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ ∅ 𝐵𝐶))
32fveq2d 6910 . . 3 (𝑦 = ∅ → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)))
4 mpteq1 5235 . . . 4 (𝑦 = ∅ → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
54fveq2d 6910 . . 3 (𝑦 = ∅ → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
63, 5eqeq12d 2753 . 2 (𝑦 = ∅ → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))))
7 iuneq1 5008 . . . . 5 (𝑦 = 𝑧 𝑥𝑦 𝐵 = 𝑥𝑧 𝐵)
87mpteq1d 5237 . . . 4 (𝑦 = 𝑧 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝑧 𝐵𝐶))
98fveq2d 6910 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)))
10 mpteq1 5235 . . . 4 (𝑦 = 𝑧 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))
1110fveq2d 6910 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
129, 11eqeq12d 2753 . 2 (𝑦 = 𝑧 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))))
13 iuneq1 5008 . . . . 5 (𝑦 = (𝑧 ∪ {𝑤}) → 𝑥𝑦 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
1413mpteq1d 5237 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶))
1514fveq2d 6910 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)))
16 mpteq1 5235 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))
1716fveq2d 6910 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
1815, 17eqeq12d 2753 . 2 (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
19 iuneq1 5008 . . . . 5 (𝑦 = 𝐴 𝑥𝑦 𝐵 = 𝑥𝐴 𝐵)
2019mpteq1d 5237 . . . 4 (𝑦 = 𝐴 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶))
2120fveq2d 6910 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
22 mpteq1 5235 . . . 4 (𝑦 = 𝐴 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
2322fveq2d 6910 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
2421, 23eqeq12d 2753 . 2 (𝑦 = 𝐴 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
25 0iun 5063 . . . . . . 7 𝑥 ∈ ∅ 𝐵 = ∅
26 mpteq1 5235 . . . . . . 7 ( 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
2725, 26ax-mp 5 . . . . . 6 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28 mpt0 6710 . . . . . 6 (𝑘 ∈ ∅ ↦ 𝐶) = ∅
2927, 28eqtri 2765 . . . . 5 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = ∅
3029fveq2i 6909 . . . 4 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘∅)
31 mpt0 6710 . . . . 5 (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))) = ∅
3231fveq2i 6909 . . . 4 ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘∅)
3330, 32eqtr4i 2768 . . 3 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
3433a1i 11 . 2 (𝜑 → (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
35 nfv 1914 . . . . . . 7 𝑥(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
36 nfcv 2905 . . . . . . . 8 𝑥Σ^
37 nfiu1 5027 . . . . . . . . 9 𝑥 𝑥 ∈ {𝑤}𝐵
38 nfcv 2905 . . . . . . . . 9 𝑥𝐶
3937, 38nfmpt 5249 . . . . . . . 8 𝑥(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)
4036, 39nffv 6916 . . . . . . 7 𝑥^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
41 simprl 771 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧𝐴)
42 sge0iunmptlemfi.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
4342adantr 480 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝐴 ∈ Fin)
44 simpr 484 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧𝐴)
45 ssfi 9213 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑧𝐴) → 𝑧 ∈ Fin)
4643, 44, 45syl2anc 584 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑧 ∈ Fin)
4741, 46syldan 591 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧 ∈ Fin)
48 simprr 773 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑤 ∈ (𝐴𝑧))
49 eldifn 4132 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → ¬ 𝑤𝑧)
50 disjsn 4711 . . . . . . . . . . 11 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5149, 50sylibr 234 . . . . . . . . . 10 (𝑤 ∈ (𝐴𝑧) → (𝑧 ∩ {𝑤}) = ∅)
5251adantl 481 . . . . . . . . 9 ((𝑧𝐴𝑤 ∈ (𝐴𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
5352adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
5453, 50sylib 218 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ¬ 𝑤𝑧)
55 simpll 767 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝜑)
56 ssel2 3978 . . . . . . . . . . 11 ((𝑧𝐴𝑥𝑧) → 𝑥𝐴)
5756adantll 714 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝑥𝐴)
58 sge0iunmptlemfi.re . . . . . . . . . 10 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
5955, 57, 58syl2anc 584 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
6059recnd 11289 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
6160adantlrr 721 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
62 csbeq1a 3913 . . . . . . . . . 10 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
63 nfcsb1v 3923 . . . . . . . . . . 11 𝑥𝑤 / 𝑥𝐵
64 vex 3484 . . . . . . . . . . 11 𝑤 ∈ V
6563, 64, 62iunxsnf 45069 . . . . . . . . . 10 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
6662, 65eqtr4di 2795 . . . . . . . . 9 (𝑥 = 𝑤𝐵 = 𝑥 ∈ {𝑤}𝐵)
6766mpteq1d 5237 . . . . . . . 8 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
6867fveq2d 6910 . . . . . . 7 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)))
6965mpteq1i 5238 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶)
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
7170fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
72 eldifi 4131 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑤𝐴)
73 nfv 1914 . . . . . . . . . . . . 13 𝑥(𝜑𝑤𝐴)
7463, 38nfmpt 5249 . . . . . . . . . . . . . . 15 𝑥(𝑘𝑤 / 𝑥𝐵𝐶)
7536, 74nffv 6916 . . . . . . . . . . . . . 14 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶))
76 nfcv 2905 . . . . . . . . . . . . . 14 𝑥
7775, 76nfel 2920 . . . . . . . . . . . . 13 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ
7873, 77nfim 1896 . . . . . . . . . . . 12 𝑥((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
79 eleq1w 2824 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
8079anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
8167, 69eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
8281fveq2d 6910 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
8382eleq1d 2826 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ↔ (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ))
8480, 83imbi12d 344 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ) ↔ ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)))
8578, 84, 58chvarfv 2240 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8672, 85sylan2 593 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8771, 86eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8887adantrl 716 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8988recnd 11289 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℂ)
9035, 40, 47, 48, 54, 61, 68, 89fsumsplitsn 15780 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
9190eqcomd 2743 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
9291adantr 480 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
93 iunxun 5094 . . . . . . . . . 10 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
9493mpteq1i 5238 . . . . . . . . 9 (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) = (𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
9594fveq2i 6909 . . . . . . . 8 ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
9695a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97 nfv 1914 . . . . . . . 8 𝑘(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
98 sge0iunmptlemfi.b . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵𝑉)
9998ralrimiva 3146 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
100 iunexg 7988 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑥𝐴 𝐵 ∈ V)
10142, 99, 100syl2anc 584 . . . . . . . . . . 11 (𝜑 𝑥𝐴 𝐵 ∈ V)
102101adantr 480 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝐴 𝐵 ∈ V)
103 iunss1 5006 . . . . . . . . . . 11 (𝑧𝐴 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
104103adantl 481 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
105102, 104ssexd 5324 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 ∈ V)
106105adantrr 717 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥𝑧 𝐵 ∈ V)
107101adantr 480 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥𝐴 𝐵 ∈ V)
108 snssi 4808 . . . . . . . . . . . . 13 (𝑤𝐴 → {𝑤} ⊆ 𝐴)
10972, 108syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴𝑧) → {𝑤} ⊆ 𝐴)
110 iunss1 5006 . . . . . . . . . . . 12 ({𝑤} ⊆ 𝐴 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
111109, 110syl 17 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
112111adantl 481 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
113107, 112ssexd 5324 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
114113adantrl 716 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
115 sge0iunmptlemfi.dj . . . . . . . . . 10 (𝜑Disj 𝑥𝐴 𝐵)
116115adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Disj 𝑥𝐴 𝐵)
117109ad2antll 729 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ⊆ 𝐴)
118 disjiun 5131 . . . . . . . . 9 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
119116, 41, 117, 53, 118syl13anc 1374 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
120 eliun 4995 . . . . . . . . . . . 12 (𝑘 𝑥𝑧 𝐵 ↔ ∃𝑥𝑧 𝑘𝐵)
121120biimpi 216 . . . . . . . . . . 11 (𝑘 𝑥𝑧 𝐵 → ∃𝑥𝑧 𝑘𝐵)
122121adantl 481 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → ∃𝑥𝑧 𝑘𝐵)
123 simp1l 1198 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝜑)
124573adant3 1133 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑥𝐴)
125 simp3 1139 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑘𝐵)
126 sge0iunmptlemfi.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
127123, 124, 125, 126syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1281273exp 1120 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝑥𝑧 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
129128rexlimdv 3153 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
130129adantr 480 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
131122, 130mpd 15 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132131adantlrr 721 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133 eliun 4995 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘𝐵)
134133biimpi 216 . . . . . . . . . . 11 (𝑘 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘𝐵)
135134adantl 481 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘𝐵)
136 simp1l 1198 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝜑)
137109sselda 3983 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
138137adantll 714 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
1391383adant3 1133 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑥𝐴)
140 simp3 1139 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑘𝐵)
141136, 139, 140, 126syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1421413exp 1120 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑥 ∈ {𝑤} → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
143142rexlimdv 3153 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
144143adantr 480 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
145135, 144mpd 15 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146145adantlrl 720 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
14797, 106, 114, 119, 132, 146sge0splitmpt 46426 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
14896, 147eqtrd 2777 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
149148adantr 480 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
150 id 22 . . . . . . . . 9 ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
151150adantl 481 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
1521263expa 1119 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
153 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
154152, 153fmptd 7134 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
15598, 154sge0ge0 46399 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
15658, 155jca 511 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
157 elrege0 13494 . . . . . . . . . . . . 13 ((Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞) ↔ ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
158156, 157sylibr 234 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
15955, 57, 158syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
160 eqid 2737 . . . . . . . . . . 11 (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
161159, 160fmptd 7134 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))):𝑧⟶(0[,)+∞))
16246, 161sge0fsum 46402 . . . . . . . . 9 ((𝜑𝑧𝐴) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
163162adantr 480 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
164 fveq2 6906 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
165 nfmpt1 5250 . . . . . . . . . . . . 13 𝑥(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
166 nfcv 2905 . . . . . . . . . . . . 13 𝑥𝑦
167165, 166nffv 6916 . . . . . . . . . . . 12 𝑥((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦)
168 nfcv 2905 . . . . . . . . . . . 12 𝑦((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
169164, 167, 168cbvsum 15731 . . . . . . . . . . 11 Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
170169a1i 11 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
171 id 22 . . . . . . . . . . . . . 14 (𝑥𝑧𝑥𝑧)
172 fvexd 6921 . . . . . . . . . . . . . 14 (𝑥𝑧 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
173160fvmpt2 7027 . . . . . . . . . . . . . 14 ((𝑥𝑧 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
174171, 172, 173syl2anc 584 . . . . . . . . . . . . 13 (𝑥𝑧 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
175174adantl 481 . . . . . . . . . . . 12 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
176175ralrimiva 3146 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → ∀𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
177176sumeq2d 15737 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
178170, 177eqtrd 2777 . . . . . . . . 9 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
179178adantr 480 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
180151, 163, 1793eqtrd 2781 . . . . . . 7 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
181180adantlrr 721 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
182181oveq1d 7446 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
18346, 59fsumrecl 15770 . . . . . . . 8 ((𝜑𝑧𝐴) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
184183adantrr 717 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
185 rexadd 13274 . . . . . . 7 ((Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
186184, 88, 185syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
187186adantr 480 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
188149, 182, 1873eqtrd 2781 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
189 snfi 9083 . . . . . . . 8 {𝑤} ∈ Fin
190189a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ∈ Fin)
191 unfi 9211 . . . . . . 7 ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
19247, 190, 191syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
193 simpll 767 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
19456ad4ant14 752 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥𝑧) → 𝑥𝐴)
195 simpll 767 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑤 ∈ (𝐴𝑧))
196 elunnel1 4154 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 ∈ {𝑤})
197 elsni 4643 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
198196, 197syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
199198adantll 714 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
200 simpr 484 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
20172adantr 480 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑤𝐴)
202200, 201eqeltrd 2841 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥𝐴)
203195, 199, 202syl2anc 584 . . . . . . . . . 10 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
204203adantlll 718 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
205194, 204pm2.61dan 813 . . . . . . . 8 (((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
206205adantll 714 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
207193, 206, 158syl2anc 584 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
208192, 207sge0fsummpt 46405 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
209208adantr 480 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
21092, 188, 2093eqtr4d 2787 . . 3 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
211210ex 412 . 2 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
2126, 12, 18, 24, 34, 211, 42findcard2d 9206 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  csb 3899  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626   ciun 4991  Disj wdisj 5110   class class class wbr 5143  cmpt 5225  cfv 6561  (class class class)co 7431  Fincfn 8985  cc 11153  cr 11154  0cc0 11155   + caddc 11158  +∞cpnf 11292  cle 11296   +𝑒 cxad 13152  [,)cico 13389  [,]cicc 13390  Σcsu 15722  Σ^csumge0 46377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-xadd 13155  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-sumge0 46378
This theorem is referenced by:  sge0iunmptlemre  46430
  Copyright terms: Public domain W3C validator