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 30470
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 3271 . . . . 5 𝑘{𝑘𝐴 ∣ ¬ 𝐵 = ∅}
2 esumrnmpt2.1 . . . . 5 (𝑦 = 𝐵𝐶 = 𝐷)
3 esumrnmpt2.2 . . . . . 6 (𝜑𝐴𝑉)
4 ssrab2 3836 . . . . . . 7 {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴
54a1i 11 . . . . . 6 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴)
63, 5ssexd 4939 . . . . 5 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V)
75sselda 3752 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
8 esumrnmpt2.3 . . . . . 6 ((𝜑𝑘𝐴) → 𝐷 ∈ (0[,]+∞))
97, 8syldan 571 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
10 esumrnmpt2.4 . . . . . . 7 ((𝜑𝑘𝐴) → 𝐵𝑊)
117, 10syldan 571 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵𝑊)
12 rabid 3264 . . . . . . . . 9 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↔ (𝑘𝐴 ∧ ¬ 𝐵 = ∅))
1312simprbi 478 . . . . . . . 8 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ 𝐵 = ∅)
1413adantl 467 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 = ∅)
15 elsng 4330 . . . . . . . 8 (𝐵𝑊 → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1611, 15syl 17 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1714, 16mtbird 314 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 ∈ {∅})
1811, 17eldifd 3734 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ (𝑊 ∖ {∅}))
19 esumrnmpt2.6 . . . . . 6 (𝜑Disj 𝑘𝐴 𝐵)
20 nfcv 2913 . . . . . . 7 𝑘𝐴
211, 20disjss1f 29724 . . . . . 6 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 → (Disj 𝑘𝐴 𝐵Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵))
225, 19, 21sylc 65 . . . . 5 (𝜑Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵)
231, 2, 6, 9, 18, 22esumrnmpt 30454 . . . 4 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
24 nfv 1995 . . . . . . . . . . 11 𝑦(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
25 snex 5036 . . . . . . . . . . . 12 {∅} ∈ V
2625a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → {∅} ∈ V)
27 velsn 4332 . . . . . . . . . . . . . . 15 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
2827biimpi 206 . . . . . . . . . . . . . 14 (𝑦 ∈ {∅} → 𝑦 = ∅)
2928adantl 467 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝑦 = ∅)
30 nfv 1995 . . . . . . . . . . . . . . . 16 𝑘𝜑
31 nfre1 3153 . . . . . . . . . . . . . . . 16 𝑘𝑘𝐴 𝐵 = ∅
3230, 31nfan 1980 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
33 nfv 1995 . . . . . . . . . . . . . . 15 𝑘 𝑦 = ∅
3432, 33nfan 1980 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅)
35 nfv 1995 . . . . . . . . . . . . . 14 𝑘 𝐶 = 0
36 simpllr 752 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = ∅)
37 simpr 471 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐵 = ∅)
3836, 37eqtr4d 2808 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = 𝐵)
3938, 2syl 17 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 𝐷)
40 simp-4l 760 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝜑)
41 simplr 744 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑘𝐴)
42 esumrnmpt2.5 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4340, 41, 37, 42syl21anc 1475 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4439, 43eqtrd 2805 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 0)
45 simplr 744 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → ∃𝑘𝐴 𝐵 = ∅)
4634, 35, 44, 45r19.29af2 3223 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → 𝐶 = 0)
4729, 46syldan 571 . . . . . . . . . . . 12 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 = 0)
48 0e0iccpnf 12490 . . . . . . . . . . . 12 0 ∈ (0[,]+∞)
4947, 48syl6eqel 2858 . . . . . . . . . . 11 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 ∈ (0[,]+∞))
50 nfcv 2913 . . . . . . . . . . . . . . . . 17 𝑘𝑦
51 nfmpt1 4881 . . . . . . . . . . . . . . . . . 18 𝑘(𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5251nfrn 5506 . . . . . . . . . . . . . . . . 17 𝑘ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5350, 52nfel 2926 . . . . . . . . . . . . . . . 16 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5430, 53nfan 1980 . . . . . . . . . . . . . . 15 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵))
55 simpr 471 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵)
56 rabid 3264 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↔ (𝑘𝐴𝐵 = ∅))
5756simprbi 478 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} → 𝐵 = ∅)
5857ad2antlr 698 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐵 = ∅)
5955, 58eqtrd 2805 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = ∅)
6059, 27sylibr 224 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 ∈ {∅})
61 vex 3354 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
62 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
6362elrnmpt 5510 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵))
6461, 63ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6564biimpi 206 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6665adantl 467 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6754, 60, 66r19.29af 3224 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝑦 ∈ {∅})
6867ex 397 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → 𝑦 ∈ {∅}))
6968ssrdv 3758 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7069adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7124, 26, 49, 70esummono 30456 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ Σ*𝑦 ∈ {∅}𝐶)
72 0ex 4924 . . . . . . . . . . . 12 ∅ ∈ V
7372a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ∅ ∈ V)
7448a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → 0 ∈ (0[,]+∞))
7546, 73, 74esumsn 30467 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ {∅}𝐶 = 0)
7671, 75breqtrd 4812 . . . . . . . . 9 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
77 simpr 471 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → ¬ ∃𝑘𝐴 𝐵 = ∅)
78 nfv 1995 . . . . . . . . . . . . 13 𝑦 ¬ ∃𝑘𝐴 𝐵 = ∅
7931nfn 1935 . . . . . . . . . . . . . . . . 17 𝑘 ¬ ∃𝑘𝐴 𝐵 = ∅
80 rabn0 4104 . . . . . . . . . . . . . . . . . . 19 ({𝑘𝐴𝐵 = ∅} ≠ ∅ ↔ ∃𝑘𝐴 𝐵 = ∅)
8180biimpi 206 . . . . . . . . . . . . . . . . . 18 ({𝑘𝐴𝐵 = ∅} ≠ ∅ → ∃𝑘𝐴 𝐵 = ∅)
8281necon1bi 2971 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → {𝑘𝐴𝐵 = ∅} = ∅)
83 eqid 2771 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
8483a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → 𝐵 = 𝐵)
8579, 82, 84mpteq12d 4868 . . . . . . . . . . . . . . . 16 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵))
86 mpt0 6161 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ∅ ↦ 𝐵) = ∅
8785, 86syl6eq 2821 . . . . . . . . . . . . . . 15 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
8887rneqd 5491 . . . . . . . . . . . . . 14 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ran ∅)
89 rn0 5515 . . . . . . . . . . . . . 14 ran ∅ = ∅
9088, 89syl6eq 2821 . . . . . . . . . . . . 13 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
9178, 90esumeq1d 30437 . . . . . . . . . . . 12 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑦 ∈ ∅𝐶)
92 esumnul 30450 . . . . . . . . . . . 12 Σ*𝑦 ∈ ∅𝐶 = 0
9391, 92syl6eq 2821 . . . . . . . . . . 11 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
94 0le0 11312 . . . . . . . . . . 11 0 ≤ 0
9593, 94syl6eqbr 4825 . . . . . . . . . 10 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9677, 95syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9776, 96pm2.61dan 796 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
98 ssrab2 3836 . . . . . . . . . . . . 13 {𝑘𝐴𝐵 = ∅} ⊆ 𝐴
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → {𝑘𝐴𝐵 = ∅} ⊆ 𝐴)
1003, 99ssexd 4939 . . . . . . . . . . 11 (𝜑 → {𝑘𝐴𝐵 = ∅} ∈ V)
101 nfrab1 3271 . . . . . . . . . . . 12 𝑘{𝑘𝐴𝐵 = ∅}
102101mptexgf 6629 . . . . . . . . . . 11 ({𝑘𝐴𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
103 rnexg 7245 . . . . . . . . . . 11 ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
104100, 102, 1033syl 18 . . . . . . . . . 10 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
1052adantl 467 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
106 simplll 750 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
10799sselda 3752 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
108107adantlr 686 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
109108adantr 466 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
110106, 109, 8syl2anc 565 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
111105, 110eqeltrd 2850 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
11254, 111, 66r19.29af 3224 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
113112ralrimiva 3115 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
114 nfcv 2913 . . . . . . . . . . 11 𝑦ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
115114esumcl 30432 . . . . . . . . . 10 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
116104, 113, 115syl2anc 565 . . . . . . . . 9 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
117 elxrge0 12488 . . . . . . . . . 10 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
118117simprbi 478 . . . . . . . . 9 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
119116, 118syl 17 . . . . . . . 8 (𝜑 → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
12097, 119jca 495 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
121 iccssxr 12461 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
122121, 116sseldi 3750 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
123121, 48sselii 3749 . . . . . . . . 9 0 ∈ ℝ*
124123a1i 11 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
125 xrletri3 12190 . . . . . . . 8 ((Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ∈ ℝ*) → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
126122, 124, 125syl2anc 565 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
127120, 126mpbird 247 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
128127oveq1d 6808 . . . . 5 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
1299ralrimiva 3115 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1301esumcl 30432 . . . . . . . . 9 (({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V ∧ ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1316, 129, 130syl2anc 565 . . . . . . . 8 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
132121, 131sseldi 3750 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ*)
13323, 132eqeltrd 2850 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
134 xaddid2 12278 . . . . . 6 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
135133, 134syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
136128, 135eqtrd 2805 . . . 4 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
137 simpl 468 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝜑)
13857adantl 467 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐵 = ∅)
139137, 107, 138, 42syl21anc 1475 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 = 0)
140139ralrimiva 3115 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
14130, 140esumeq2d 30439 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0)
142101esum0 30451 . . . . . . . 8 ({𝑘𝐴𝐵 = ∅} ∈ V → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
143100, 142syl 17 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
144141, 143eqtrd 2805 . . . . . 6 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
145144oveq1d 6808 . . . . 5 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
146 xaddid2 12278 . . . . . 6 *𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ* → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
147132, 146syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
148145, 147eqtrd 2805 . . . 4 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
14923, 136, 1483eqtr4d 2815 . . 3 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
150 nfv 1995 . . . 4 𝑦𝜑
151 nfcv 2913 . . . 4 𝑦ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
1521mptexgf 6629 . . . . 5 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
153 rnexg 7245 . . . . 5 ((𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
1546, 152, 1533syl 18 . . . 4 (𝜑 → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
15569ssrind 3988 . . . . . 6 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
156 incom 3956 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
15713neqned 2950 . . . . . . . . . . . 12 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → 𝐵 ≠ ∅)
158157necomd 2998 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ∅ ≠ 𝐵)
159158neneqd 2948 . . . . . . . . . 10 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ ∅ = 𝐵)
160159nrex 3148 . . . . . . . . 9 ¬ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵
161 eqid 2771 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
162161elrnmpt 5510 . . . . . . . . . 10 (∅ ∈ V → (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵))
16372, 162ax-mp 5 . . . . . . . . 9 (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵)
164160, 163mtbir 312 . . . . . . . 8 ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
165 disjsn 4383 . . . . . . . 8 ((ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
166164, 165mpbir 221 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅
167156, 166eqtr3i 2795 . . . . . 6 ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅
168155, 167syl6sseq 3800 . . . . 5 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅)
169 ss0 4118 . . . . 5 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅ → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
170168, 169syl 17 . . . 4 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
171 nfmpt1 4881 . . . . . . . 8 𝑘(𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
172171nfrn 5506 . . . . . . 7 𝑘ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17350, 172nfel 2926 . . . . . 6 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17430, 173nfan 1980 . . . . 5 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
1752adantl 467 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
176 simplll 750 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
1777adantlr 686 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
178177adantr 466 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
179176, 178, 8syl2anc 565 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
180175, 179eqeltrd 2850 . . . . 5 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
181161elrnmpt 5510 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵))
18261, 181ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
183182biimpi 206 . . . . . 6 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
184183adantl 467 . . . . 5 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
185174, 180, 184r19.29af 3224 . . . 4 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
186150, 114, 151, 104, 154, 170, 112, 185esumsplit 30455 . . 3 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
187 rabnc 4106 . . . . 5 ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅
188187a1i 11 . . . 4 (𝜑 → ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅)
189107, 8syldan 571 . . . 4 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
19030, 101, 1, 100, 6, 188, 189, 9esumsplit 30455 . . 3 (𝜑 → Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷 = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
191149, 186, 1903eqtr4d 2815 . 2 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
192 rabxm 4105 . . . . . . . 8 𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})
193192, 83mpteq12i 4876 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵)
194 mptun 6165 . . . . . . 7 (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
195193, 194eqtri 2793 . . . . . 6 (𝑘𝐴𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
196195rneqi 5490 . . . . 5 ran (𝑘𝐴𝐵) = ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
197 rnun 5682 . . . . 5 ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
198196, 197eqtri 2793 . . . 4 ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
199198a1i 11 . . 3 (𝜑 → ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
200150, 199esumeq1d 30437 . 2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶)
201192a1i 11 . . 3 (𝜑𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}))
20230, 201esumeq1d 30437 . 2 (𝜑 → Σ*𝑘𝐴𝐷 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
203191, 200, 2023eqtr4d 2815 1 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑘𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cun 3721  cin 3722  wss 3723  c0 4063  {csn 4316  Disj wdisj 4754   class class class wbr 4786  cmpt 4863  ran crn 5250  (class class class)co 6793  0cc0 10138  +∞cpnf 10273  *cxr 10275  cle 10277   +𝑒 cxad 12149  [,]cicc 12383  Σ*cesum 30429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-disj 4755  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14015  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428  df-sum 14625  df-ef 15004  df-sin 15006  df-cos 15007  df-pi 15009  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-ordt 16369  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-ps 17408  df-tsr 17409  df-plusf 17449  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-mhm 17543  df-submnd 17544  df-grp 17633  df-minusg 17634  df-sbg 17635  df-mulg 17749  df-subg 17799  df-cntz 17957  df-cmn 18402  df-abl 18403  df-mgp 18698  df-ur 18710  df-ring 18757  df-cring 18758  df-subrg 18988  df-abv 19027  df-lmod 19075  df-scaf 19076  df-sra 19387  df-rgmod 19388  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-tmd 22096  df-tgp 22097  df-tsms 22150  df-trg 22183  df-xms 22345  df-ms 22346  df-tms 22347  df-nm 22607  df-ngp 22608  df-nrg 22610  df-nlm 22611  df-ii 22900  df-cncf 22901  df-limc 23850  df-dv 23851  df-log 24524  df-esum 30430
This theorem is referenced by:  carsggect  30720  carsgclctunlem2  30721  pmeasadd  30727
  Copyright terms: Public domain W3C validator