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 44207
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 4952 . . . . 5 (𝑦 = ∅ → 𝑥𝑦 𝐵 = 𝑥 ∈ ∅ 𝐵)
21mpteq1d 5181 . . . 4 (𝑦 = ∅ → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ ∅ 𝐵𝐶))
32fveq2d 6815 . . 3 (𝑦 = ∅ → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)))
4 mpteq1 5179 . . . 4 (𝑦 = ∅ → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
54fveq2d 6815 . . 3 (𝑦 = ∅ → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
63, 5eqeq12d 2752 . 2 (𝑦 = ∅ → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))))
7 iuneq1 4952 . . . . 5 (𝑦 = 𝑧 𝑥𝑦 𝐵 = 𝑥𝑧 𝐵)
87mpteq1d 5181 . . . 4 (𝑦 = 𝑧 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝑧 𝐵𝐶))
98fveq2d 6815 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)))
10 mpteq1 5179 . . . 4 (𝑦 = 𝑧 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))
1110fveq2d 6815 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
129, 11eqeq12d 2752 . 2 (𝑦 = 𝑧 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))))
13 iuneq1 4952 . . . . 5 (𝑦 = (𝑧 ∪ {𝑤}) → 𝑥𝑦 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
1413mpteq1d 5181 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶))
1514fveq2d 6815 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)))
16 mpteq1 5179 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))
1716fveq2d 6815 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
1815, 17eqeq12d 2752 . 2 (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
19 iuneq1 4952 . . . . 5 (𝑦 = 𝐴 𝑥𝑦 𝐵 = 𝑥𝐴 𝐵)
2019mpteq1d 5181 . . . 4 (𝑦 = 𝐴 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶))
2120fveq2d 6815 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
22 mpteq1 5179 . . . 4 (𝑦 = 𝐴 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
2322fveq2d 6815 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
2421, 23eqeq12d 2752 . 2 (𝑦 = 𝐴 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
25 0iun 5004 . . . . . . 7 𝑥 ∈ ∅ 𝐵 = ∅
26 mpteq1 5179 . . . . . . 7 ( 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
2725, 26ax-mp 5 . . . . . 6 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28 mpt0 6612 . . . . . 6 (𝑘 ∈ ∅ ↦ 𝐶) = ∅
2927, 28eqtri 2764 . . . . 5 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = ∅
3029fveq2i 6814 . . . 4 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘∅)
31 mpt0 6612 . . . . 5 (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))) = ∅
3231fveq2i 6814 . . . 4 ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘∅)
3330, 32eqtr4i 2767 . . 3 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
3433a1i 11 . 2 (𝜑 → (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
35 nfv 1916 . . . . . . 7 𝑥(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
36 nfcv 2904 . . . . . . . 8 𝑥Σ^
37 nfiu1 4970 . . . . . . . . 9 𝑥 𝑥 ∈ {𝑤}𝐵
38 nfcv 2904 . . . . . . . . 9 𝑥𝐶
3937, 38nfmpt 5193 . . . . . . . 8 𝑥(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)
4036, 39nffv 6821 . . . . . . 7 𝑥^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
41 simprl 768 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧𝐴)
42 sge0iunmptlemfi.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
4342adantr 481 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝐴 ∈ Fin)
44 simpr 485 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧𝐴)
45 ssfi 9016 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑧𝐴) → 𝑧 ∈ Fin)
4643, 44, 45syl2anc 584 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑧 ∈ Fin)
4741, 46syldan 591 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧 ∈ Fin)
48 simprr 770 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑤 ∈ (𝐴𝑧))
49 eldifn 4072 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → ¬ 𝑤𝑧)
50 disjsn 4656 . . . . . . . . . . 11 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5149, 50sylibr 233 . . . . . . . . . 10 (𝑤 ∈ (𝐴𝑧) → (𝑧 ∩ {𝑤}) = ∅)
5251adantl 482 . . . . . . . . 9 ((𝑧𝐴𝑤 ∈ (𝐴𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
5352adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
5453, 50sylib 217 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ¬ 𝑤𝑧)
55 simpll 764 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝜑)
56 ssel2 3925 . . . . . . . . . . 11 ((𝑧𝐴𝑥𝑧) → 𝑥𝐴)
5756adantll 711 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝑥𝐴)
58 sge0iunmptlemfi.re . . . . . . . . . 10 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
5955, 57, 58syl2anc 584 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
6059recnd 11082 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
6160adantlrr 718 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
62 csbeq1a 3855 . . . . . . . . . 10 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
63 nfcsb1v 3866 . . . . . . . . . . 11 𝑥𝑤 / 𝑥𝐵
64 vex 3444 . . . . . . . . . . 11 𝑤 ∈ V
6563, 64, 62iunxsnf 42851 . . . . . . . . . 10 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
6662, 65eqtr4di 2794 . . . . . . . . 9 (𝑥 = 𝑤𝐵 = 𝑥 ∈ {𝑤}𝐵)
6766mpteq1d 5181 . . . . . . . 8 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
6867fveq2d 6815 . . . . . . 7 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)))
6965mpteq1i 5182 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶)
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
7170fveq2d 6815 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
72 eldifi 4071 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑤𝐴)
73 nfv 1916 . . . . . . . . . . . . 13 𝑥(𝜑𝑤𝐴)
7463, 38nfmpt 5193 . . . . . . . . . . . . . . 15 𝑥(𝑘𝑤 / 𝑥𝐵𝐶)
7536, 74nffv 6821 . . . . . . . . . . . . . 14 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶))
76 nfcv 2904 . . . . . . . . . . . . . 14 𝑥
7775, 76nfel 2918 . . . . . . . . . . . . 13 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ
7873, 77nfim 1898 . . . . . . . . . . . 12 𝑥((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
79 eleq1w 2819 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
8079anbi2d 629 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
8167, 69eqtrdi 2792 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
8281fveq2d 6815 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
8382eleq1d 2821 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ↔ (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ))
8480, 83imbi12d 344 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ) ↔ ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)))
8578, 84, 58chvarfv 2232 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8672, 85sylan2 593 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8771, 86eqeltrd 2837 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8887adantrl 713 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8988recnd 11082 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℂ)
9035, 40, 47, 48, 54, 61, 68, 89fsumsplitsn 15532 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
9190eqcomd 2742 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
9291adantr 481 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
93 iunxun 5035 . . . . . . . . . 10 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
9493mpteq1i 5182 . . . . . . . . 9 (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) = (𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
9594fveq2i 6814 . . . . . . . 8 ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
9695a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97 nfv 1916 . . . . . . . 8 𝑘(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
98 sge0iunmptlemfi.b . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵𝑉)
9998ralrimiva 3139 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
100 iunexg 7852 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑥𝐴 𝐵 ∈ V)
10142, 99, 100syl2anc 584 . . . . . . . . . . 11 (𝜑 𝑥𝐴 𝐵 ∈ V)
102101adantr 481 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝐴 𝐵 ∈ V)
103 iunss1 4950 . . . . . . . . . . 11 (𝑧𝐴 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
104103adantl 482 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
105102, 104ssexd 5262 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 ∈ V)
106105adantrr 714 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥𝑧 𝐵 ∈ V)
107101adantr 481 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥𝐴 𝐵 ∈ V)
108 snssi 4752 . . . . . . . . . . . . 13 (𝑤𝐴 → {𝑤} ⊆ 𝐴)
10972, 108syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴𝑧) → {𝑤} ⊆ 𝐴)
110 iunss1 4950 . . . . . . . . . . . 12 ({𝑤} ⊆ 𝐴 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
111109, 110syl 17 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
112111adantl 482 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
113107, 112ssexd 5262 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
114113adantrl 713 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
115 sge0iunmptlemfi.dj . . . . . . . . . 10 (𝜑Disj 𝑥𝐴 𝐵)
116115adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Disj 𝑥𝐴 𝐵)
117109ad2antll 726 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ⊆ 𝐴)
118 disjiun 5073 . . . . . . . . 9 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
119116, 41, 117, 53, 118syl13anc 1371 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
120 eliun 4940 . . . . . . . . . . . 12 (𝑘 𝑥𝑧 𝐵 ↔ ∃𝑥𝑧 𝑘𝐵)
121120biimpi 215 . . . . . . . . . . 11 (𝑘 𝑥𝑧 𝐵 → ∃𝑥𝑧 𝑘𝐵)
122121adantl 482 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → ∃𝑥𝑧 𝑘𝐵)
123 simp1l 1196 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝜑)
124573adant3 1131 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑥𝐴)
125 simp3 1137 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑘𝐵)
126 sge0iunmptlemfi.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
127123, 124, 125, 126syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1281273exp 1118 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝑥𝑧 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
129128rexlimdv 3146 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
130129adantr 481 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
131122, 130mpd 15 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132131adantlrr 718 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133 eliun 4940 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘𝐵)
134133biimpi 215 . . . . . . . . . . 11 (𝑘 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘𝐵)
135134adantl 482 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘𝐵)
136 simp1l 1196 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝜑)
137109sselda 3930 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
138137adantll 711 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
1391383adant3 1131 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑥𝐴)
140 simp3 1137 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑘𝐵)
141136, 139, 140, 126syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1421413exp 1118 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑥 ∈ {𝑤} → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
143142rexlimdv 3146 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
144143adantr 481 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
145135, 144mpd 15 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146145adantlrl 717 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
14797, 106, 114, 119, 132, 146sge0splitmpt 44205 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
14896, 147eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
149148adantr 481 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
150 id 22 . . . . . . . . 9 ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
151150adantl 482 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
1521263expa 1117 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
153 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
154152, 153fmptd 7027 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
15598, 154sge0ge0 44178 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
15658, 155jca 512 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
157 elrege0 13265 . . . . . . . . . . . . 13 ((Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞) ↔ ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
158156, 157sylibr 233 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
15955, 57, 158syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
160 eqid 2736 . . . . . . . . . . 11 (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
161159, 160fmptd 7027 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))):𝑧⟶(0[,)+∞))
16246, 161sge0fsum 44181 . . . . . . . . 9 ((𝜑𝑧𝐴) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
163162adantr 481 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
164 fveq2 6811 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
165 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑧
166 nfcv 2904 . . . . . . . . . . . 12 𝑦𝑧
167 nfmpt1 5194 . . . . . . . . . . . . 13 𝑥(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
168 nfcv 2904 . . . . . . . . . . . . 13 𝑥𝑦
169167, 168nffv 6821 . . . . . . . . . . . 12 𝑥((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦)
170 nfcv 2904 . . . . . . . . . . . 12 𝑦((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
171164, 165, 166, 169, 170cbvsum 15483 . . . . . . . . . . 11 Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
172171a1i 11 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
173 id 22 . . . . . . . . . . . . . 14 (𝑥𝑧𝑥𝑧)
174 fvexd 6826 . . . . . . . . . . . . . 14 (𝑥𝑧 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
175160fvmpt2 6925 . . . . . . . . . . . . . 14 ((𝑥𝑧 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
176173, 174, 175syl2anc 584 . . . . . . . . . . . . 13 (𝑥𝑧 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
177176adantl 482 . . . . . . . . . . . 12 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
178177ralrimiva 3139 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → ∀𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
179178sumeq2d 15490 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
180172, 179eqtrd 2776 . . . . . . . . 9 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
181180adantr 481 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
182151, 163, 1813eqtrd 2780 . . . . . . 7 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
183182adantlrr 718 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
184183oveq1d 7331 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
18546, 59fsumrecl 15522 . . . . . . . 8 ((𝜑𝑧𝐴) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
186185adantrr 714 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
187 rexadd 13045 . . . . . . 7 ((Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
188186, 88, 187syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
189188adantr 481 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
190149, 184, 1893eqtrd 2780 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
191 snfi 8887 . . . . . . . 8 {𝑤} ∈ Fin
192191a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ∈ Fin)
193 unfi 9015 . . . . . . 7 ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
19447, 192, 193syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
195 simpll 764 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
19656ad4ant14 749 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥𝑧) → 𝑥𝐴)
197 simpll 764 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑤 ∈ (𝐴𝑧))
198 elunnel1 4094 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 ∈ {𝑤})
199 elsni 4587 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
200198, 199syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
201200adantll 711 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
202 simpr 485 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
20372adantr 481 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑤𝐴)
204202, 203eqeltrd 2837 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥𝐴)
205197, 201, 204syl2anc 584 . . . . . . . . . 10 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
206205adantlll 715 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
207196, 206pm2.61dan 810 . . . . . . . 8 (((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
208207adantll 711 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
209195, 208, 158syl2anc 584 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
210194, 209sge0fsummpt 44184 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
211210adantr 481 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
21292, 190, 2113eqtr4d 2786 . . 3 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
213212ex 413 . 2 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
2146, 12, 18, 24, 34, 213, 42findcard2d 9009 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  wral 3061  wrex 3070  Vcvv 3440  csb 3841  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  {csn 4570   ciun 4936  Disj wdisj 5051   class class class wbr 5086  cmpt 5169  cfv 6465  (class class class)co 7316  Fincfn 8782  cc 10948  cr 10949  0cc0 10950   + caddc 10953  +∞cpnf 11085  cle 11089   +𝑒 cxad 12925  [,)cico 13160  [,]cicc 13161  Σcsu 15473  Σ^csumge0 44156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-inf2 9476  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-disj 5052  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-sup 9277  df-oi 9345  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-n0 12313  df-z 12399  df-uz 12662  df-rp 12810  df-xadd 12928  df-ico 13164  df-icc 13165  df-fz 13319  df-fzo 13462  df-seq 13801  df-exp 13862  df-hash 14124  df-cj 14886  df-re 14887  df-im 14888  df-sqrt 15022  df-abs 15023  df-clim 15273  df-sum 15474  df-sumge0 44157
This theorem is referenced by:  sge0iunmptlemre  44209
  Copyright terms: Public domain W3C validator