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 41133
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 4686 . . . . 5 (𝑦 = ∅ → 𝑥𝑦 𝐵 = 𝑥 ∈ ∅ 𝐵)
21mpteq1d 4890 . . . 4 (𝑦 = ∅ → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ ∅ 𝐵𝐶))
32fveq2d 6356 . . 3 (𝑦 = ∅ → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)))
4 mpteq1 4889 . . . 4 (𝑦 = ∅ → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
54fveq2d 6356 . . 3 (𝑦 = ∅ → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
63, 5eqeq12d 2775 . 2 (𝑦 = ∅ → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))))
7 iuneq1 4686 . . . . 5 (𝑦 = 𝑧 𝑥𝑦 𝐵 = 𝑥𝑧 𝐵)
87mpteq1d 4890 . . . 4 (𝑦 = 𝑧 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝑧 𝐵𝐶))
98fveq2d 6356 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)))
10 mpteq1 4889 . . . 4 (𝑦 = 𝑧 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))
1110fveq2d 6356 . . 3 (𝑦 = 𝑧 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
129, 11eqeq12d 2775 . 2 (𝑦 = 𝑧 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))))
13 iuneq1 4686 . . . . 5 (𝑦 = (𝑧 ∪ {𝑤}) → 𝑥𝑦 𝐵 = 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
1413mpteq1d 4890 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶))
1514fveq2d 6356 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)))
16 mpteq1 4889 . . . 4 (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))
1716fveq2d 6356 . . 3 (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
1815, 17eqeq12d 2775 . 2 (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
19 iuneq1 4686 . . . . 5 (𝑦 = 𝐴 𝑥𝑦 𝐵 = 𝑥𝐴 𝐵)
2019mpteq1d 4890 . . . 4 (𝑦 = 𝐴 → (𝑘 𝑥𝑦 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶))
2120fveq2d 6356 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
22 mpteq1 4889 . . . 4 (𝑦 = 𝐴 → (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
2322fveq2d 6356 . . 3 (𝑦 = 𝐴 → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
2421, 23eqeq12d 2775 . 2 (𝑦 = 𝐴 → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
25 0iun 4729 . . . . . . 7 𝑥 ∈ ∅ 𝐵 = ∅
26 mpteq1 4889 . . . . . . 7 ( 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
2725, 26ax-mp 5 . . . . . 6 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28 mpt0 6182 . . . . . 6 (𝑘 ∈ ∅ ↦ 𝐶) = ∅
2927, 28eqtri 2782 . . . . 5 (𝑘 𝑥 ∈ ∅ 𝐵𝐶) = ∅
3029fveq2i 6355 . . . 4 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘∅)
31 mpt0 6182 . . . . 5 (𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))) = ∅
3231fveq2i 6355 . . . 4 ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘∅)
3330, 32eqtr4i 2785 . . 3 ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶))))
3433a1i 11 . 2 (𝜑 → (Σ^‘(𝑘 𝑥 ∈ ∅ 𝐵𝐶)) = (Σ^‘(𝑥 ∈ ∅ ↦ (Σ^‘(𝑘𝐵𝐶)))))
35 nfv 1992 . . . . . . 7 𝑥(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
36 nfcv 2902 . . . . . . . 8 𝑥Σ^
37 nfiu1 4702 . . . . . . . . 9 𝑥 𝑥 ∈ {𝑤}𝐵
38 nfcv 2902 . . . . . . . . 9 𝑥𝐶
3937, 38nfmpt 4898 . . . . . . . 8 𝑥(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)
4036, 39nffv 6359 . . . . . . 7 𝑥^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
41 simprl 811 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧𝐴)
42 sge0iunmptlemfi.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
4342adantr 472 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝐴 ∈ Fin)
44 simpr 479 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑧𝐴)
45 ssfi 8345 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑧𝐴) → 𝑧 ∈ Fin)
4643, 44, 45syl2anc 696 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑧 ∈ Fin)
4741, 46syldan 488 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑧 ∈ Fin)
48 simprr 813 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑤 ∈ (𝐴𝑧))
49 eldifn 3876 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → ¬ 𝑤𝑧)
50 disjsn 4390 . . . . . . . . . . 11 ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤𝑧)
5149, 50sylibr 224 . . . . . . . . . 10 (𝑤 ∈ (𝐴𝑧) → (𝑧 ∩ {𝑤}) = ∅)
5251adantl 473 . . . . . . . . 9 ((𝑧𝐴𝑤 ∈ (𝐴𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
5352adantl 473 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
5453, 50sylib 208 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ¬ 𝑤𝑧)
55 simpll 807 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝜑)
56 ssel2 3739 . . . . . . . . . . 11 ((𝑧𝐴𝑥𝑧) → 𝑥𝐴)
5756adantll 752 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → 𝑥𝐴)
58 sge0iunmptlemfi.re . . . . . . . . . 10 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
5955, 57, 58syl2anc 696 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
6059recnd 10260 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
6160adantlrr 759 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℂ)
62 csbeq1a 3683 . . . . . . . . . 10 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
63 nfcsb1v 3690 . . . . . . . . . . 11 𝑥𝑤 / 𝑥𝐵
64 vex 3343 . . . . . . . . . . 11 𝑤 ∈ V
6563, 64, 62iunxsnf 39732 . . . . . . . . . 10 𝑥 ∈ {𝑤}𝐵 = 𝑤 / 𝑥𝐵
6662, 65syl6eqr 2812 . . . . . . . . 9 (𝑥 = 𝑤𝐵 = 𝑥 ∈ {𝑤}𝐵)
6766mpteq1d 4890 . . . . . . . 8 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘 𝑥 ∈ {𝑤}𝐵𝐶))
6867fveq2d 6356 . . . . . . 7 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)))
6965mpteq1i 4891 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶)
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑘 𝑥 ∈ {𝑤}𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
7170fveq2d 6356 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
72 eldifi 3875 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑤𝐴)
73 nfv 1992 . . . . . . . . . . . . 13 𝑥(𝜑𝑤𝐴)
7463, 38nfmpt 4898 . . . . . . . . . . . . . . 15 𝑥(𝑘𝑤 / 𝑥𝐵𝐶)
7536, 74nffv 6359 . . . . . . . . . . . . . 14 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶))
76 nfcv 2902 . . . . . . . . . . . . . 14 𝑥
7775, 76nfel 2915 . . . . . . . . . . . . 13 𝑥^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ
7873, 77nfim 1974 . . . . . . . . . . . 12 𝑥((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
79 eleq1w 2822 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
8079anbi2d 742 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝜑𝑥𝐴) ↔ (𝜑𝑤𝐴)))
8167, 69syl6eq 2810 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑘𝐵𝐶) = (𝑘𝑤 / 𝑥𝐵𝐶))
8281fveq2d 6356 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)))
8382eleq1d 2824 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ↔ (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ))
8480, 83imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ) ↔ ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)))
8578, 84, 58chvar 2407 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8672, 85sylan2 492 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘𝑤 / 𝑥𝐵𝐶)) ∈ ℝ)
8771, 86eqeltrd 2839 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8887adantrl 754 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ)
8988recnd 10260 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℂ)
9035, 40, 47, 48, 54, 61, 68, 89fsumsplitsn 14673 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
9190eqcomd 2766 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
9291adantr 472 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
93 iunxun 4757 . . . . . . . . . 10 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵)
9493mpteq1i 4891 . . . . . . . . 9 (𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) = (𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
9594fveq2i 6355 . . . . . . . 8 ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
9695a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97 nfv 1992 . . . . . . . 8 𝑘(𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧)))
98 sge0iunmptlemfi.b . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵𝑉)
9998ralrimiva 3104 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐴 𝐵𝑉)
100 iunexg 7308 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑥𝐴 𝐵 ∈ V)
10142, 99, 100syl2anc 696 . . . . . . . . . . 11 (𝜑 𝑥𝐴 𝐵 ∈ V)
102101adantr 472 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝐴 𝐵 ∈ V)
103 iunss1 4684 . . . . . . . . . . 11 (𝑧𝐴 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
104103adantl 473 . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 𝑥𝐴 𝐵)
105102, 104ssexd 4957 . . . . . . . . 9 ((𝜑𝑧𝐴) → 𝑥𝑧 𝐵 ∈ V)
106105adantrr 755 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥𝑧 𝐵 ∈ V)
107101adantr 472 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥𝐴 𝐵 ∈ V)
108 snssi 4484 . . . . . . . . . . . . 13 (𝑤𝐴 → {𝑤} ⊆ 𝐴)
10972, 108syl 17 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴𝑧) → {𝑤} ⊆ 𝐴)
110 iunss1 4684 . . . . . . . . . . . 12 ({𝑤} ⊆ 𝐴 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
111109, 110syl 17 . . . . . . . . . . 11 (𝑤 ∈ (𝐴𝑧) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
112111adantl 473 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 𝑥𝐴 𝐵)
113107, 112ssexd 4957 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐴𝑧)) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
114113adantrl 754 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → 𝑥 ∈ {𝑤}𝐵 ∈ V)
115 sge0iunmptlemfi.dj . . . . . . . . . 10 (𝜑Disj 𝑥𝐴 𝐵)
116115adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Disj 𝑥𝐴 𝐵)
117109ad2antll 767 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ⊆ 𝐴)
118 disjiun 4792 . . . . . . . . 9 ((Disj 𝑥𝐴 𝐵 ∧ (𝑧𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
119116, 41, 117, 53, 118syl13anc 1479 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) = ∅)
120 eliun 4676 . . . . . . . . . . . 12 (𝑘 𝑥𝑧 𝐵 ↔ ∃𝑥𝑧 𝑘𝐵)
121120biimpi 206 . . . . . . . . . . 11 (𝑘 𝑥𝑧 𝐵 → ∃𝑥𝑧 𝑘𝐵)
122121adantl 473 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → ∃𝑥𝑧 𝑘𝐵)
123 simp1l 1240 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝜑)
124573adant3 1127 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑥𝐴)
125 simp3 1133 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝑘𝐵)
126 sge0iunmptlemfi.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
127123, 124, 125, 126syl3anc 1477 . . . . . . . . . . . . 13 (((𝜑𝑧𝐴) ∧ 𝑥𝑧𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1281273exp 1113 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝑥𝑧 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
129128rexlimdv 3168 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
130129adantr 472 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → (∃𝑥𝑧 𝑘𝐵𝐶 ∈ (0[,]+∞)))
131122, 130mpd 15 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132131adantlrr 759 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133 eliun 4676 . . . . . . . . . . . 12 (𝑘 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘𝐵)
134133biimpi 206 . . . . . . . . . . 11 (𝑘 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘𝐵)
135134adantl 473 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘𝐵)
136 simp1l 1240 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝜑)
137109sselda 3744 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
138137adantll 752 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥𝐴)
1391383adant3 1127 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑥𝐴)
140 simp3 1133 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝑘𝐵)
141136, 139, 140, 126syl3anc 1477 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
1421413exp 1113 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴𝑧)) → (𝑥 ∈ {𝑤} → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
143142rexlimdv 3168 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴𝑧)) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
144143adantr 472 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘𝐵𝐶 ∈ (0[,]+∞)))
145135, 144mpd 15 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴𝑧)) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146145adantlrl 758 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑘 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
14797, 106, 114, 119, 132, 146sge0splitmpt 41131 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 ∈ ( 𝑥𝑧 𝐵 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
14896, 147eqtrd 2794 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
149148adantr 472 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
150 id 22 . . . . . . . . 9 ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
151150adantl 473 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))))
1521263expa 1112 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
153 eqid 2760 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
154152, 153fmptd 6548 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
15598, 154sge0ge0 41104 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
15658, 155jca 555 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
157 elrege0 12471 . . . . . . . . . . . . 13 ((Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞) ↔ ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^‘(𝑘𝐵𝐶))))
158156, 157sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
15955, 57, 158syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
160 eqid 2760 . . . . . . . . . . 11 (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
161159, 160fmptd 6548 . . . . . . . . . 10 ((𝜑𝑧𝐴) → (𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))):𝑧⟶(0[,)+∞))
16246, 161sge0fsum 41107 . . . . . . . . 9 ((𝜑𝑧𝐴) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
163162adantr 472 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦))
164 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = 𝑥 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
165 nfcv 2902 . . . . . . . . . . . 12 𝑥𝑧
166 nfcv 2902 . . . . . . . . . . . 12 𝑦𝑧
167 nfmpt1 4899 . . . . . . . . . . . . 13 𝑥(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))
168 nfcv 2902 . . . . . . . . . . . . 13 𝑥𝑦
169167, 168nffv 6359 . . . . . . . . . . . 12 𝑥((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦)
170 nfcv 2902 . . . . . . . . . . . 12 𝑦((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
171164, 165, 166, 169, 170cbvsum 14624 . . . . . . . . . . 11 Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥)
172171a1i 11 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥))
173 id 22 . . . . . . . . . . . . . 14 (𝑥𝑧𝑥𝑧)
174 fvexd 6364 . . . . . . . . . . . . . 14 (𝑥𝑧 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
175160fvmpt2 6453 . . . . . . . . . . . . . 14 ((𝑥𝑧 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
176173, 174, 175syl2anc 696 . . . . . . . . . . . . 13 (𝑥𝑧 → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
177176adantl 473 . . . . . . . . . . . 12 (((𝜑𝑧𝐴) ∧ 𝑥𝑧) → ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
178177ralrimiva 3104 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → ∀𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = (Σ^‘(𝑘𝐵𝐶)))
179178sumeq2d 14631 . . . . . . . . . 10 ((𝜑𝑧𝐴) → Σ𝑥𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑥) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
180172, 179eqtrd 2794 . . . . . . . . 9 ((𝜑𝑧𝐴) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
181180adantr 472 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → Σ𝑦𝑧 ((𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))‘𝑦) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
182151, 163, 1813eqtrd 2798 . . . . . . 7 (((𝜑𝑧𝐴) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
183182adantlrr 759 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = Σ𝑥𝑧^‘(𝑘𝐵𝐶)))
184183oveq1d 6828 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
18546, 59fsumrecl 14664 . . . . . . . 8 ((𝜑𝑧𝐴) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
186185adantrr 755 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ)
187 rexadd 12256 . . . . . . 7 ((Σ𝑥𝑧^‘(𝑘𝐵𝐶)) ∈ ℝ ∧ (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶)) ∈ ℝ) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
188186, 88, 187syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
189188adantr 472 . . . . 5 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) +𝑒^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
190149, 184, 1893eqtrd 2798 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ𝑥𝑧^‘(𝑘𝐵𝐶)) + (Σ^‘(𝑘 𝑥 ∈ {𝑤}𝐵𝐶))))
191 snfi 8203 . . . . . . . 8 {𝑤} ∈ Fin
192191a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → {𝑤} ∈ Fin)
193 unfi 8392 . . . . . . 7 ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
19447, 192, 193syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
195 simpll 807 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
19656ad4ant14 1209 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥𝑧) → 𝑥𝐴)
197 simpll 807 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑤 ∈ (𝐴𝑧))
198 elunnel1 3897 . . . . . . . . . . . . 13 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 ∈ {𝑤})
199 elsni 4338 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
200198, 199syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
201200adantll 752 . . . . . . . . . . 11 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥 = 𝑤)
202 simpr 479 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
20372adantr 472 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑤𝐴)
204202, 203eqeltrd 2839 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 = 𝑤) → 𝑥𝐴)
205197, 201, 204syl2anc 696 . . . . . . . . . 10 (((𝑤 ∈ (𝐴𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
206205adantlll 756 . . . . . . . . 9 ((((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥𝑧) → 𝑥𝐴)
207196, 206pm2.61dan 867 . . . . . . . 8 (((𝑧𝐴𝑤 ∈ (𝐴𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
208207adantll 752 . . . . . . 7 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥𝐴)
209195, 208, 158syl2anc 696 . . . . . 6 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
210194, 209sge0fsummpt 41110 . . . . 5 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
211210adantr 472 . . . 4 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^‘(𝑘𝐵𝐶)))
21292, 190, 2113eqtr4d 2804 . . 3 (((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) ∧ (Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶))))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶)))))
213212ex 449 . 2 ((𝜑 ∧ (𝑧𝐴𝑤 ∈ (𝐴𝑧))) → ((Σ^‘(𝑘 𝑥𝑧 𝐵𝐶)) = (Σ^‘(𝑥𝑧 ↦ (Σ^‘(𝑘𝐵𝐶)))) → (Σ^‘(𝑘 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶)) = (Σ^‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^‘(𝑘𝐵𝐶))))))
2146, 12, 18, 24, 34, 213, 42findcard2d 8367 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  wrex 3051  Vcvv 3340  csb 3674  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058  {csn 4321   ciun 4672  Disj wdisj 4772   class class class wbr 4804  cmpt 4881  cfv 6049  (class class class)co 6813  Fincfn 8121  cc 10126  cr 10127  0cc0 10128   + caddc 10131  +∞cpnf 10263  cle 10267   +𝑒 cxad 12137  [,)cico 12370  [,]cicc 12371  Σcsu 14615  Σ^csumge0 41082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-xadd 12140  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-sumge0 41083
This theorem is referenced by:  sge0iunmptlemre  41135
  Copyright terms: Public domain W3C validator