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 33379
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 3450 . . . . 5 𝑘{𝑘𝐴 ∣ ¬ 𝐵 = ∅}
2 esumrnmpt2.1 . . . . 5 (𝑦 = 𝐵𝐶 = 𝐷)
3 esumrnmpt2.2 . . . . . 6 (𝜑𝐴𝑉)
4 ssrab2 4077 . . . . . . 7 {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴
54a1i 11 . . . . . 6 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴)
63, 5ssexd 5324 . . . . 5 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V)
75sselda 3982 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
8 esumrnmpt2.3 . . . . . 6 ((𝜑𝑘𝐴) → 𝐷 ∈ (0[,]+∞))
97, 8syldan 590 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
10 esumrnmpt2.4 . . . . . . 7 ((𝜑𝑘𝐴) → 𝐵𝑊)
117, 10syldan 590 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵𝑊)
12 rabid 3451 . . . . . . . . 9 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↔ (𝑘𝐴 ∧ ¬ 𝐵 = ∅))
1312simprbi 496 . . . . . . . 8 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ 𝐵 = ∅)
1413adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 = ∅)
15 elsng 4642 . . . . . . . 8 (𝐵𝑊 → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1611, 15syl 17 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1714, 16mtbird 325 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 ∈ {∅})
1811, 17eldifd 3959 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ (𝑊 ∖ {∅}))
19 esumrnmpt2.6 . . . . . 6 (𝜑Disj 𝑘𝐴 𝐵)
20 nfcv 2902 . . . . . . 7 𝑘𝐴
211, 20disjss1f 32085 . . . . . 6 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 → (Disj 𝑘𝐴 𝐵Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵))
225, 19, 21sylc 65 . . . . 5 (𝜑Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵)
231, 2, 6, 9, 18, 22esumrnmpt 33363 . . . 4 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
24 nfv 1916 . . . . . . . . . . 11 𝑦(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
25 snex 5431 . . . . . . . . . . . 12 {∅} ∈ V
2625a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → {∅} ∈ V)
27 velsn 4644 . . . . . . . . . . . . . . 15 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
2827biimpi 215 . . . . . . . . . . . . . 14 (𝑦 ∈ {∅} → 𝑦 = ∅)
2928adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝑦 = ∅)
30 nfv 1916 . . . . . . . . . . . . . . . 16 𝑘𝜑
31 nfre1 3281 . . . . . . . . . . . . . . . 16 𝑘𝑘𝐴 𝐵 = ∅
3230, 31nfan 1901 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
33 nfv 1916 . . . . . . . . . . . . . . 15 𝑘 𝑦 = ∅
3432, 33nfan 1901 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅)
35 nfv 1916 . . . . . . . . . . . . . 14 𝑘 𝐶 = 0
36 simpllr 773 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = ∅)
37 simpr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐵 = ∅)
3836, 37eqtr4d 2774 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = 𝐵)
3938, 2syl 17 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 𝐷)
40 simp-4l 780 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝜑)
41 simplr 766 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑘𝐴)
42 esumrnmpt2.5 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4340, 41, 37, 42syl21anc 835 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4439, 43eqtrd 2771 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 0)
45 simplr 766 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → ∃𝑘𝐴 𝐵 = ∅)
4634, 35, 44, 45r19.29af2 3263 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → 𝐶 = 0)
4729, 46syldan 590 . . . . . . . . . . . 12 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 = 0)
48 0e0iccpnf 13443 . . . . . . . . . . . 12 0 ∈ (0[,]+∞)
4947, 48eqeltrdi 2840 . . . . . . . . . . 11 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 ∈ (0[,]+∞))
50 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑘𝑦
51 nfmpt1 5256 . . . . . . . . . . . . . . . . . 18 𝑘(𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5251nfrn 5951 . . . . . . . . . . . . . . . . 17 𝑘ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5350, 52nfel 2916 . . . . . . . . . . . . . . . 16 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5430, 53nfan 1901 . . . . . . . . . . . . . . 15 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵))
55 simpr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵)
56 rabid 3451 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↔ (𝑘𝐴𝐵 = ∅))
5756simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} → 𝐵 = ∅)
5857ad2antlr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐵 = ∅)
5955, 58eqtrd 2771 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = ∅)
6059, 27sylibr 233 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 ∈ {∅})
61 vex 3477 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
62 eqid 2731 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
6362elrnmpt 5955 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵))
6461, 63ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6564biimpi 215 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6665adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6754, 60, 66r19.29af 3264 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝑦 ∈ {∅})
6867ex 412 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → 𝑦 ∈ {∅}))
6968ssrdv 3988 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7069adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7124, 26, 49, 70esummono 33365 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ Σ*𝑦 ∈ {∅}𝐶)
72 0ex 5307 . . . . . . . . . . . 12 ∅ ∈ V
7372a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ∅ ∈ V)
7448a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → 0 ∈ (0[,]+∞))
7546, 73, 74esumsn 33376 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ {∅}𝐶 = 0)
7671, 75breqtrd 5174 . . . . . . . . 9 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
77 simpr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → ¬ ∃𝑘𝐴 𝐵 = ∅)
78 nfv 1916 . . . . . . . . . . . . 13 𝑦 ¬ ∃𝑘𝐴 𝐵 = ∅
7931nfn 1859 . . . . . . . . . . . . . . . . 17 𝑘 ¬ ∃𝑘𝐴 𝐵 = ∅
80 rabn0 4385 . . . . . . . . . . . . . . . . . . 19 ({𝑘𝐴𝐵 = ∅} ≠ ∅ ↔ ∃𝑘𝐴 𝐵 = ∅)
8180biimpi 215 . . . . . . . . . . . . . . . . . 18 ({𝑘𝐴𝐵 = ∅} ≠ ∅ → ∃𝑘𝐴 𝐵 = ∅)
8281necon1bi 2968 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → {𝑘𝐴𝐵 = ∅} = ∅)
83 eqid 2731 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
8483a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → 𝐵 = 𝐵)
8579, 82, 84mpteq12df 5234 . . . . . . . . . . . . . . . 16 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵))
86 mpt0 6692 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ∅ ↦ 𝐵) = ∅
8785, 86eqtrdi 2787 . . . . . . . . . . . . . . 15 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
8887rneqd 5937 . . . . . . . . . . . . . 14 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ran ∅)
89 rn0 5925 . . . . . . . . . . . . . 14 ran ∅ = ∅
9088, 89eqtrdi 2787 . . . . . . . . . . . . 13 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
9178, 90esumeq1d 33346 . . . . . . . . . . . 12 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑦 ∈ ∅𝐶)
92 esumnul 33359 . . . . . . . . . . . 12 Σ*𝑦 ∈ ∅𝐶 = 0
9391, 92eqtrdi 2787 . . . . . . . . . . 11 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
94 0le0 12320 . . . . . . . . . . 11 0 ≤ 0
9593, 94eqbrtrdi 5187 . . . . . . . . . 10 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9677, 95syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9776, 96pm2.61dan 810 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
98 ssrab2 4077 . . . . . . . . . . . . 13 {𝑘𝐴𝐵 = ∅} ⊆ 𝐴
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → {𝑘𝐴𝐵 = ∅} ⊆ 𝐴)
1003, 99ssexd 5324 . . . . . . . . . . 11 (𝜑 → {𝑘𝐴𝐵 = ∅} ∈ V)
101 nfrab1 3450 . . . . . . . . . . . 12 𝑘{𝑘𝐴𝐵 = ∅}
102101mptexgf 7226 . . . . . . . . . . 11 ({𝑘𝐴𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
103 rnexg 7899 . . . . . . . . . . 11 ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
104100, 102, 1033syl 18 . . . . . . . . . 10 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
1052adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
106 simplll 772 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
10799sselda 3982 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
108107adantlr 712 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
109108adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
110106, 109, 8syl2anc 583 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
111105, 110eqeltrd 2832 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
11254, 111, 66r19.29af 3264 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
113112ralrimiva 3145 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
114 nfcv 2902 . . . . . . . . . . 11 𝑦ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
115114esumcl 33341 . . . . . . . . . 10 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
116104, 113, 115syl2anc 583 . . . . . . . . 9 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
117 elxrge0 13441 . . . . . . . . . 10 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
118117simprbi 496 . . . . . . . . 9 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
119116, 118syl 17 . . . . . . . 8 (𝜑 → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
12097, 119jca 511 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
121 iccssxr 13414 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
122121, 116sselid 3980 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
123121, 48sselii 3979 . . . . . . . . 9 0 ∈ ℝ*
124123a1i 11 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
125 xrletri3 13140 . . . . . . . 8 ((Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ∈ ℝ*) → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
126122, 124, 125syl2anc 583 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
127120, 126mpbird 257 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
128127oveq1d 7427 . . . . 5 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
1299ralrimiva 3145 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1301esumcl 33341 . . . . . . . . 9 (({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V ∧ ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1316, 129, 130syl2anc 583 . . . . . . . 8 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
132121, 131sselid 3980 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ*)
13323, 132eqeltrd 2832 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
134 xaddlid 13228 . . . . . 6 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
135133, 134syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
136128, 135eqtrd 2771 . . . 4 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
137 simpl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝜑)
13857adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐵 = ∅)
139137, 107, 138, 42syl21anc 835 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 = 0)
140139ralrimiva 3145 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
14130, 140esumeq2d 33348 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0)
142101esum0 33360 . . . . . . . 8 ({𝑘𝐴𝐵 = ∅} ∈ V → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
143100, 142syl 17 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
144141, 143eqtrd 2771 . . . . . 6 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
145144oveq1d 7427 . . . . 5 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
146 xaddlid 13228 . . . . . 6 *𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ* → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
147132, 146syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
148145, 147eqtrd 2771 . . . 4 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
14923, 136, 1483eqtr4d 2781 . . 3 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
150 nfv 1916 . . . 4 𝑦𝜑
151 nfcv 2902 . . . 4 𝑦ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
1521mptexgf 7226 . . . . 5 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
153 rnexg 7899 . . . . 5 ((𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
1546, 152, 1533syl 18 . . . 4 (𝜑 → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
15569ssrind 4235 . . . . . 6 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
156 incom 4201 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
15713neqned 2946 . . . . . . . . . . . 12 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → 𝐵 ≠ ∅)
158157necomd 2995 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ∅ ≠ 𝐵)
159158neneqd 2944 . . . . . . . . . 10 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ ∅ = 𝐵)
160159nrex 3073 . . . . . . . . 9 ¬ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵
161 eqid 2731 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
162161elrnmpt 5955 . . . . . . . . . 10 (∅ ∈ V → (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵))
16372, 162ax-mp 5 . . . . . . . . 9 (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵)
164160, 163mtbir 323 . . . . . . . 8 ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
165 disjsn 4715 . . . . . . . 8 ((ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
166164, 165mpbir 230 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅
167156, 166eqtr3i 2761 . . . . . 6 ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅
168155, 167sseqtrdi 4032 . . . . 5 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅)
169 ss0 4398 . . . . 5 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅ → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
170168, 169syl 17 . . . 4 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
171 nfmpt1 5256 . . . . . . . 8 𝑘(𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
172171nfrn 5951 . . . . . . 7 𝑘ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17350, 172nfel 2916 . . . . . 6 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17430, 173nfan 1901 . . . . 5 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
1752adantl 481 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
176 simplll 772 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
1777adantlr 712 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
178177adantr 480 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
179176, 178, 8syl2anc 583 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
180175, 179eqeltrd 2832 . . . . 5 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
181161elrnmpt 5955 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵))
18261, 181ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
183182biimpi 215 . . . . . 6 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
184183adantl 481 . . . . 5 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
185174, 180, 184r19.29af 3264 . . . 4 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
186150, 114, 151, 104, 154, 170, 112, 185esumsplit 33364 . . 3 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
187 rabnc 4387 . . . . 5 ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅
188187a1i 11 . . . 4 (𝜑 → ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅)
189107, 8syldan 590 . . . 4 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
19030, 101, 1, 100, 6, 188, 189, 9esumsplit 33364 . . 3 (𝜑 → Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷 = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
191149, 186, 1903eqtr4d 2781 . 2 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
192 rabxm 4386 . . . . . . . 8 𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})
193192, 83mpteq12i 5254 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵)
194 mptun 6696 . . . . . . 7 (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
195193, 194eqtri 2759 . . . . . 6 (𝑘𝐴𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
196195rneqi 5936 . . . . 5 ran (𝑘𝐴𝐵) = ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
197 rnun 6145 . . . . 5 ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
198196, 197eqtri 2759 . . . 4 ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
199198a1i 11 . . 3 (𝜑 → ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
200150, 199esumeq1d 33346 . 2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶)
201192a1i 11 . . 3 (𝜑𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}))
20230, 201esumeq1d 33346 . 2 (𝜑 → Σ*𝑘𝐴𝐷 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
203191, 200, 2023eqtr4d 2781 1 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑘𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  {crab 3431  Vcvv 3473  cun 3946  cin 3947  wss 3948  c0 4322  {csn 4628  Disj wdisj 5113   class class class wbr 5148  cmpt 5231  ran crn 5677  (class class class)co 7412  0cc0 11116  +∞cpnf 11252  *cxr 11254  cle 11256   +𝑒 cxad 13097  [,]cicc 13334  Σ*cesum 33338
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 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194  ax-addf 11195  ax-mulf 11196
This theorem depends on definitions:  df-bi 206  df-an 396  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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8152  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-2o 8473  df-er 8709  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9368  df-fi 9412  df-sup 9443  df-inf 9444  df-oi 9511  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-ioo 13335  df-ioc 13336  df-ico 13337  df-icc 13338  df-fz 13492  df-fzo 13635  df-fl 13764  df-mod 13842  df-seq 13974  df-exp 14035  df-fac 14241  df-bc 14270  df-hash 14298  df-shft 15021  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-limsup 15422  df-clim 15439  df-rlim 15440  df-sum 15640  df-ef 16018  df-sin 16020  df-cos 16021  df-pi 16023  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-rest 17375  df-topn 17376  df-0g 17394  df-gsum 17395  df-topgen 17396  df-pt 17397  df-prds 17400  df-ordt 17454  df-xrs 17455  df-qtop 17460  df-imas 17461  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-ps 18526  df-tsr 18527  df-plusf 18567  df-mgm 18568  df-sgrp 18647  df-mnd 18663  df-mhm 18708  df-submnd 18709  df-grp 18861  df-minusg 18862  df-sbg 18863  df-mulg 18991  df-subg 19043  df-cntz 19226  df-cmn 19695  df-abl 19696  df-mgp 20033  df-rng 20051  df-ur 20080  df-ring 20133  df-cring 20134  df-subrng 20438  df-subrg 20463  df-abv 20572  df-lmod 20620  df-scaf 20621  df-sra 20934  df-rgmod 20935  df-psmet 21140  df-xmet 21141  df-met 21142  df-bl 21143  df-mopn 21144  df-fbas 21145  df-fg 21146  df-cnfld 21149  df-top 22629  df-topon 22646  df-topsp 22668  df-bases 22682  df-cld 22756  df-ntr 22757  df-cls 22758  df-nei 22835  df-lp 22873  df-perf 22874  df-cn 22964  df-cnp 22965  df-haus 23052  df-tx 23299  df-hmeo 23492  df-fil 23583  df-fm 23675  df-flim 23676  df-flf 23677  df-tmd 23809  df-tgp 23810  df-tsms 23864  df-trg 23897  df-xms 24059  df-ms 24060  df-tms 24061  df-nm 24324  df-ngp 24325  df-nrg 24327  df-nlm 24328  df-ii 24630  df-cncf 24631  df-limc 25628  df-dv 25629  df-log 26316  df-esum 33339
This theorem is referenced by:  carsggect  33630  carsgclctunlem2  33631  pmeasadd  33637
  Copyright terms: Public domain W3C validator