Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumrnmpt2 Structured version   Visualization version   GIF version

Theorem esumrnmpt2 32428
Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020.)
Hypotheses
Ref Expression
esumrnmpt2.1 (𝑦 = 𝐵𝐶 = 𝐷)
esumrnmpt2.2 (𝜑𝐴𝑉)
esumrnmpt2.3 ((𝜑𝑘𝐴) → 𝐷 ∈ (0[,]+∞))
esumrnmpt2.4 ((𝜑𝑘𝐴) → 𝐵𝑊)
esumrnmpt2.5 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
esumrnmpt2.6 (𝜑Disj 𝑘𝐴 𝐵)
Assertion
Ref Expression
esumrnmpt2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑘𝐴𝐷)
Distinct variable groups:   𝐴,𝑘,𝑦   𝑦,𝐵   𝐶,𝑘   𝑦,𝐷   𝑘,𝑊   𝜑,𝑘,𝑦
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑦)   𝐷(𝑘)   𝑉(𝑦,𝑘)   𝑊(𝑦)

Proof of Theorem esumrnmpt2
StepHypRef Expression
1 nfrab1 3425 . . . . 5 𝑘{𝑘𝐴 ∣ ¬ 𝐵 = ∅}
2 esumrnmpt2.1 . . . . 5 (𝑦 = 𝐵𝐶 = 𝐷)
3 esumrnmpt2.2 . . . . . 6 (𝜑𝐴𝑉)
4 ssrab2 4036 . . . . . . 7 {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴
54a1i 11 . . . . . 6 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴)
63, 5ssexd 5280 . . . . 5 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V)
75sselda 3943 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
8 esumrnmpt2.3 . . . . . 6 ((𝜑𝑘𝐴) → 𝐷 ∈ (0[,]+∞))
97, 8syldan 592 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
10 esumrnmpt2.4 . . . . . . 7 ((𝜑𝑘𝐴) → 𝐵𝑊)
117, 10syldan 592 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵𝑊)
12 rabid 3426 . . . . . . . . 9 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↔ (𝑘𝐴 ∧ ¬ 𝐵 = ∅))
1312simprbi 498 . . . . . . . 8 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ 𝐵 = ∅)
1413adantl 483 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 = ∅)
15 elsng 4599 . . . . . . . 8 (𝐵𝑊 → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1611, 15syl 17 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1714, 16mtbird 325 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 ∈ {∅})
1811, 17eldifd 3920 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ (𝑊 ∖ {∅}))
19 esumrnmpt2.6 . . . . . 6 (𝜑Disj 𝑘𝐴 𝐵)
20 nfcv 2906 . . . . . . 7 𝑘𝐴
211, 20disjss1f 31275 . . . . . 6 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 → (Disj 𝑘𝐴 𝐵Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵))
225, 19, 21sylc 65 . . . . 5 (𝜑Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵)
231, 2, 6, 9, 18, 22esumrnmpt 32412 . . . 4 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
24 nfv 1918 . . . . . . . . . . 11 𝑦(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
25 snex 5387 . . . . . . . . . . . 12 {∅} ∈ V
2625a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → {∅} ∈ V)
27 velsn 4601 . . . . . . . . . . . . . . 15 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
2827biimpi 215 . . . . . . . . . . . . . 14 (𝑦 ∈ {∅} → 𝑦 = ∅)
2928adantl 483 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝑦 = ∅)
30 nfv 1918 . . . . . . . . . . . . . . . 16 𝑘𝜑
31 nfre1 3267 . . . . . . . . . . . . . . . 16 𝑘𝑘𝐴 𝐵 = ∅
3230, 31nfan 1903 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
33 nfv 1918 . . . . . . . . . . . . . . 15 𝑘 𝑦 = ∅
3432, 33nfan 1903 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅)
35 nfv 1918 . . . . . . . . . . . . . 14 𝑘 𝐶 = 0
36 simpllr 775 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = ∅)
37 simpr 486 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐵 = ∅)
3836, 37eqtr4d 2781 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = 𝐵)
3938, 2syl 17 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 𝐷)
40 simp-4l 782 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝜑)
41 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑘𝐴)
42 esumrnmpt2.5 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4340, 41, 37, 42syl21anc 837 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4439, 43eqtrd 2778 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 0)
45 simplr 768 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → ∃𝑘𝐴 𝐵 = ∅)
4634, 35, 44, 45r19.29af2 3249 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → 𝐶 = 0)
4729, 46syldan 592 . . . . . . . . . . . 12 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 = 0)
48 0e0iccpnf 13305 . . . . . . . . . . . 12 0 ∈ (0[,]+∞)
4947, 48eqeltrdi 2847 . . . . . . . . . . 11 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 ∈ (0[,]+∞))
50 nfcv 2906 . . . . . . . . . . . . . . . . 17 𝑘𝑦
51 nfmpt1 5212 . . . . . . . . . . . . . . . . . 18 𝑘(𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5251nfrn 5904 . . . . . . . . . . . . . . . . 17 𝑘ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5350, 52nfel 2920 . . . . . . . . . . . . . . . 16 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5430, 53nfan 1903 . . . . . . . . . . . . . . 15 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵))
55 simpr 486 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵)
56 rabid 3426 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↔ (𝑘𝐴𝐵 = ∅))
5756simprbi 498 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} → 𝐵 = ∅)
5857ad2antlr 726 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐵 = ∅)
5955, 58eqtrd 2778 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = ∅)
6059, 27sylibr 233 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 ∈ {∅})
61 vex 3448 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
62 eqid 2738 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
6362elrnmpt 5908 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵))
6461, 63ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6564biimpi 215 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6665adantl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6754, 60, 66r19.29af 3250 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝑦 ∈ {∅})
6867ex 414 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → 𝑦 ∈ {∅}))
6968ssrdv 3949 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7069adantr 482 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7124, 26, 49, 70esummono 32414 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ Σ*𝑦 ∈ {∅}𝐶)
72 0ex 5263 . . . . . . . . . . . 12 ∅ ∈ V
7372a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ∅ ∈ V)
7448a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → 0 ∈ (0[,]+∞))
7546, 73, 74esumsn 32425 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ {∅}𝐶 = 0)
7671, 75breqtrd 5130 . . . . . . . . 9 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
77 simpr 486 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → ¬ ∃𝑘𝐴 𝐵 = ∅)
78 nfv 1918 . . . . . . . . . . . . 13 𝑦 ¬ ∃𝑘𝐴 𝐵 = ∅
7931nfn 1861 . . . . . . . . . . . . . . . . 17 𝑘 ¬ ∃𝑘𝐴 𝐵 = ∅
80 rabn0 4344 . . . . . . . . . . . . . . . . . . 19 ({𝑘𝐴𝐵 = ∅} ≠ ∅ ↔ ∃𝑘𝐴 𝐵 = ∅)
8180biimpi 215 . . . . . . . . . . . . . . . . . 18 ({𝑘𝐴𝐵 = ∅} ≠ ∅ → ∃𝑘𝐴 𝐵 = ∅)
8281necon1bi 2971 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → {𝑘𝐴𝐵 = ∅} = ∅)
83 eqid 2738 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
8483a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → 𝐵 = 𝐵)
8579, 82, 84mpteq12df 5190 . . . . . . . . . . . . . . . 16 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵))
86 mpt0 6639 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ∅ ↦ 𝐵) = ∅
8785, 86eqtrdi 2794 . . . . . . . . . . . . . . 15 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
8887rneqd 5890 . . . . . . . . . . . . . 14 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ran ∅)
89 rn0 5878 . . . . . . . . . . . . . 14 ran ∅ = ∅
9088, 89eqtrdi 2794 . . . . . . . . . . . . 13 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
9178, 90esumeq1d 32395 . . . . . . . . . . . 12 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑦 ∈ ∅𝐶)
92 esumnul 32408 . . . . . . . . . . . 12 Σ*𝑦 ∈ ∅𝐶 = 0
9391, 92eqtrdi 2794 . . . . . . . . . . 11 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
94 0le0 12188 . . . . . . . . . . 11 0 ≤ 0
9593, 94eqbrtrdi 5143 . . . . . . . . . 10 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9677, 95syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9776, 96pm2.61dan 812 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
98 ssrab2 4036 . . . . . . . . . . . . 13 {𝑘𝐴𝐵 = ∅} ⊆ 𝐴
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → {𝑘𝐴𝐵 = ∅} ⊆ 𝐴)
1003, 99ssexd 5280 . . . . . . . . . . 11 (𝜑 → {𝑘𝐴𝐵 = ∅} ∈ V)
101 nfrab1 3425 . . . . . . . . . . . 12 𝑘{𝑘𝐴𝐵 = ∅}
102101mptexgf 7167 . . . . . . . . . . 11 ({𝑘𝐴𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
103 rnexg 7832 . . . . . . . . . . 11 ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
104100, 102, 1033syl 18 . . . . . . . . . 10 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
1052adantl 483 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
106 simplll 774 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
10799sselda 3943 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
108107adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
109108adantr 482 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
110106, 109, 8syl2anc 585 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
111105, 110eqeltrd 2839 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
11254, 111, 66r19.29af 3250 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
113112ralrimiva 3142 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
114 nfcv 2906 . . . . . . . . . . 11 𝑦ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
115114esumcl 32390 . . . . . . . . . 10 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
116104, 113, 115syl2anc 585 . . . . . . . . 9 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
117 elxrge0 13303 . . . . . . . . . 10 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
118117simprbi 498 . . . . . . . . 9 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
119116, 118syl 17 . . . . . . . 8 (𝜑 → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
12097, 119jca 513 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
121 iccssxr 13276 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
122121, 116sselid 3941 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
123121, 48sselii 3940 . . . . . . . . 9 0 ∈ ℝ*
124123a1i 11 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
125 xrletri3 13002 . . . . . . . 8 ((Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ∈ ℝ*) → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
126122, 124, 125syl2anc 585 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
127120, 126mpbird 257 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
128127oveq1d 7365 . . . . 5 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
1299ralrimiva 3142 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1301esumcl 32390 . . . . . . . . 9 (({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V ∧ ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1316, 129, 130syl2anc 585 . . . . . . . 8 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
132121, 131sselid 3941 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ*)
13323, 132eqeltrd 2839 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
134 xaddid2 13090 . . . . . 6 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
135133, 134syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
136128, 135eqtrd 2778 . . . 4 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
137 simpl 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝜑)
13857adantl 483 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐵 = ∅)
139137, 107, 138, 42syl21anc 837 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 = 0)
140139ralrimiva 3142 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
14130, 140esumeq2d 32397 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0)
142101esum0 32409 . . . . . . . 8 ({𝑘𝐴𝐵 = ∅} ∈ V → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
143100, 142syl 17 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
144141, 143eqtrd 2778 . . . . . 6 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
145144oveq1d 7365 . . . . 5 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
146 xaddid2 13090 . . . . . 6 *𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ* → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
147132, 146syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
148145, 147eqtrd 2778 . . . 4 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
14923, 136, 1483eqtr4d 2788 . . 3 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
150 nfv 1918 . . . 4 𝑦𝜑
151 nfcv 2906 . . . 4 𝑦ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
1521mptexgf 7167 . . . . 5 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
153 rnexg 7832 . . . . 5 ((𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
1546, 152, 1533syl 18 . . . 4 (𝜑 → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
15569ssrind 4194 . . . . . 6 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
156 incom 4160 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
15713neqned 2949 . . . . . . . . . . . 12 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → 𝐵 ≠ ∅)
158157necomd 2998 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ∅ ≠ 𝐵)
159158neneqd 2947 . . . . . . . . . 10 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ ∅ = 𝐵)
160159nrex 3076 . . . . . . . . 9 ¬ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵
161 eqid 2738 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
162161elrnmpt 5908 . . . . . . . . . 10 (∅ ∈ V → (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵))
16372, 162ax-mp 5 . . . . . . . . 9 (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵)
164160, 163mtbir 323 . . . . . . . 8 ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
165 disjsn 4671 . . . . . . . 8 ((ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
166164, 165mpbir 230 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅
167156, 166eqtr3i 2768 . . . . . 6 ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅
168155, 167sseqtrdi 3993 . . . . 5 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅)
169 ss0 4357 . . . . 5 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅ → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
170168, 169syl 17 . . . 4 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
171 nfmpt1 5212 . . . . . . . 8 𝑘(𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
172171nfrn 5904 . . . . . . 7 𝑘ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17350, 172nfel 2920 . . . . . 6 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17430, 173nfan 1903 . . . . 5 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
1752adantl 483 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
176 simplll 774 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
1777adantlr 714 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
178177adantr 482 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
179176, 178, 8syl2anc 585 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
180175, 179eqeltrd 2839 . . . . 5 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
181161elrnmpt 5908 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵))
18261, 181ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
183182biimpi 215 . . . . . 6 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
184183adantl 483 . . . . 5 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
185174, 180, 184r19.29af 3250 . . . 4 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
186150, 114, 151, 104, 154, 170, 112, 185esumsplit 32413 . . 3 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
187 rabnc 4346 . . . . 5 ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅
188187a1i 11 . . . 4 (𝜑 → ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅)
189107, 8syldan 592 . . . 4 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
19030, 101, 1, 100, 6, 188, 189, 9esumsplit 32413 . . 3 (𝜑 → Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷 = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
191149, 186, 1903eqtr4d 2788 . 2 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
192 rabxm 4345 . . . . . . . 8 𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})
193192, 83mpteq12i 5210 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵)
194 mptun 6643 . . . . . . 7 (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
195193, 194eqtri 2766 . . . . . 6 (𝑘𝐴𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
196195rneqi 5889 . . . . 5 ran (𝑘𝐴𝐵) = ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
197 rnun 6095 . . . . 5 ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
198196, 197eqtri 2766 . . . 4 ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
199198a1i 11 . . 3 (𝜑 → ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
200150, 199esumeq1d 32395 . 2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶)
201192a1i 11 . . 3 (𝜑𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}))
20230, 201esumeq1d 32395 . 2 (𝜑 → Σ*𝑘𝐴𝐷 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
203191, 200, 2023eqtr4d 2788 1 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑘𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2942  wral 3063  wrex 3072  {crab 3406  Vcvv 3444  cun 3907  cin 3908  wss 3909  c0 4281  {csn 4585  Disj wdisj 5069   class class class wbr 5104  cmpt 5187  ran crn 5632  (class class class)co 7350  0cc0 10985  +∞cpnf 11120  *cxr 11122  cle 11124   +𝑒 cxad 12960  [,]cicc 13196  Σ*cesum 32387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064  ax-mulf 11065
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-om 7794  df-1st 7912  df-2nd 7913  df-supp 8061  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-ixp 8770  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fsupp 9240  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155  df-8 12156  df-9 12157  df-n0 12348  df-z 12434  df-dec 12552  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ioc 13198  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-mod 13704  df-seq 13836  df-exp 13897  df-fac 14102  df-bc 14131  df-hash 14159  df-shft 14886  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-limsup 15288  df-clim 15305  df-rlim 15306  df-sum 15506  df-ef 15885  df-sin 15887  df-cos 15888  df-pi 15890  df-struct 16954  df-sets 16971  df-slot 16989  df-ndx 17001  df-base 17019  df-ress 17048  df-plusg 17081  df-mulr 17082  df-starv 17083  df-sca 17084  df-vsca 17085  df-ip 17086  df-tset 17087  df-ple 17088  df-ds 17090  df-unif 17091  df-hom 17092  df-cco 17093  df-rest 17239  df-topn 17240  df-0g 17258  df-gsum 17259  df-topgen 17260  df-pt 17261  df-prds 17264  df-ordt 17318  df-xrs 17319  df-qtop 17324  df-imas 17325  df-xps 17327  df-mre 17401  df-mrc 17402  df-acs 17404  df-ps 18390  df-tsr 18391  df-plusf 18431  df-mgm 18432  df-sgrp 18481  df-mnd 18492  df-mhm 18536  df-submnd 18537  df-grp 18686  df-minusg 18687  df-sbg 18688  df-mulg 18807  df-subg 18858  df-cntz 19029  df-cmn 19493  df-abl 19494  df-mgp 19826  df-ur 19843  df-ring 19890  df-cring 19891  df-subrg 20143  df-abv 20199  df-lmod 20247  df-scaf 20248  df-sra 20556  df-rgmod 20557  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-fbas 20716  df-fg 20717  df-cnfld 20720  df-top 22165  df-topon 22182  df-topsp 22204  df-bases 22218  df-cld 22292  df-ntr 22293  df-cls 22294  df-nei 22371  df-lp 22409  df-perf 22410  df-cn 22500  df-cnp 22501  df-haus 22588  df-tx 22835  df-hmeo 23028  df-fil 23119  df-fm 23211  df-flim 23212  df-flf 23213  df-tmd 23345  df-tgp 23346  df-tsms 23400  df-trg 23433  df-xms 23595  df-ms 23596  df-tms 23597  df-nm 23860  df-ngp 23861  df-nrg 23863  df-nlm 23864  df-ii 24162  df-cncf 24163  df-limc 25152  df-dv 25153  df-log 25834  df-esum 32388
This theorem is referenced by:  carsggect  32679  carsgclctunlem2  32680  pmeasadd  32686
  Copyright terms: Public domain W3C validator