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 30598
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 3270 . . . . 5 𝑘{𝑘𝐴 ∣ ¬ 𝐵 = ∅}
2 esumrnmpt2.1 . . . . 5 (𝑦 = 𝐵𝐶 = 𝐷)
3 esumrnmpt2.2 . . . . . 6 (𝜑𝐴𝑉)
4 ssrab2 3849 . . . . . . 7 {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴
54a1i 11 . . . . . 6 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴)
63, 5ssexd 4968 . . . . 5 (𝜑 → {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V)
75sselda 3763 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
8 esumrnmpt2.3 . . . . . 6 ((𝜑𝑘𝐴) → 𝐷 ∈ (0[,]+∞))
97, 8syldan 585 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
10 esumrnmpt2.4 . . . . . . 7 ((𝜑𝑘𝐴) → 𝐵𝑊)
117, 10syldan 585 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵𝑊)
12 rabid 3263 . . . . . . . . 9 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↔ (𝑘𝐴 ∧ ¬ 𝐵 = ∅))
1312simprbi 490 . . . . . . . 8 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ 𝐵 = ∅)
1413adantl 473 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 = ∅)
15 elsng 4350 . . . . . . . 8 (𝐵𝑊 → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1611, 15syl 17 . . . . . . 7 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → (𝐵 ∈ {∅} ↔ 𝐵 = ∅))
1714, 16mtbird 316 . . . . . 6 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → ¬ 𝐵 ∈ {∅})
1811, 17eldifd 3745 . . . . 5 ((𝜑𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝐵 ∈ (𝑊 ∖ {∅}))
19 esumrnmpt2.6 . . . . . 6 (𝜑Disj 𝑘𝐴 𝐵)
20 nfcv 2907 . . . . . . 7 𝑘𝐴
211, 20disjss1f 29855 . . . . . 6 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ⊆ 𝐴 → (Disj 𝑘𝐴 𝐵Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵))
225, 19, 21sylc 65 . . . . 5 (𝜑Disj 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐵)
231, 2, 6, 9, 18, 22esumrnmpt 30582 . . . 4 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
24 nfv 2009 . . . . . . . . . . 11 𝑦(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
25 snex 5066 . . . . . . . . . . . 12 {∅} ∈ V
2625a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → {∅} ∈ V)
27 velsn 4352 . . . . . . . . . . . . . . 15 (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
2827biimpi 207 . . . . . . . . . . . . . 14 (𝑦 ∈ {∅} → 𝑦 = ∅)
2928adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝑦 = ∅)
30 nfv 2009 . . . . . . . . . . . . . . . 16 𝑘𝜑
31 nfre1 3151 . . . . . . . . . . . . . . . 16 𝑘𝑘𝐴 𝐵 = ∅
3230, 31nfan 1998 . . . . . . . . . . . . . . 15 𝑘(𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅)
33 nfv 2009 . . . . . . . . . . . . . . 15 𝑘 𝑦 = ∅
3432, 33nfan 1998 . . . . . . . . . . . . . 14 𝑘((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅)
35 nfv 2009 . . . . . . . . . . . . . 14 𝑘 𝐶 = 0
36 simpllr 793 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = ∅)
37 simpr 477 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐵 = ∅)
3836, 37eqtr4d 2802 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑦 = 𝐵)
3938, 2syl 17 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 𝐷)
40 simp-4l 801 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝜑)
41 simplr 785 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝑘𝐴)
42 esumrnmpt2.5 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4340, 41, 37, 42syl21anc 866 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐷 = 0)
4439, 43eqtrd 2799 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) ∧ 𝑘𝐴) ∧ 𝐵 = ∅) → 𝐶 = 0)
45 simplr 785 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → ∃𝑘𝐴 𝐵 = ∅)
4634, 35, 44, 45r19.29af2 3222 . . . . . . . . . . . . 13 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 = ∅) → 𝐶 = 0)
4729, 46syldan 585 . . . . . . . . . . . 12 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 = 0)
48 0e0iccpnf 12492 . . . . . . . . . . . 12 0 ∈ (0[,]+∞)
4947, 48syl6eqel 2852 . . . . . . . . . . 11 (((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) ∧ 𝑦 ∈ {∅}) → 𝐶 ∈ (0[,]+∞))
50 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑘𝑦
51 nfmpt1 4908 . . . . . . . . . . . . . . . . . 18 𝑘(𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5251nfrn 5539 . . . . . . . . . . . . . . . . 17 𝑘ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5350, 52nfel 2920 . . . . . . . . . . . . . . . 16 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
5430, 53nfan 1998 . . . . . . . . . . . . . . 15 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵))
55 simpr 477 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵)
56 rabid 3263 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↔ (𝑘𝐴𝐵 = ∅))
5756simprbi 490 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} → 𝐵 = ∅)
5857ad2antlr 718 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐵 = ∅)
5955, 58eqtrd 2799 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 = ∅)
6059, 27sylibr 225 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑦 ∈ {∅})
61 vex 3353 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
62 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
6362elrnmpt 5543 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵))
6461, 63ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6564biimpi 207 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6665adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝑦 = 𝐵)
6754, 60, 66r19.29af 3223 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝑦 ∈ {∅})
6867ex 401 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) → 𝑦 ∈ {∅}))
6968ssrdv 3769 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7069adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ⊆ {∅})
7124, 26, 49, 70esummono 30584 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ Σ*𝑦 ∈ {∅}𝐶)
72 0ex 4952 . . . . . . . . . . . 12 ∅ ∈ V
7372a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → ∅ ∈ V)
7448a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → 0 ∈ (0[,]+∞))
7546, 73, 74esumsn 30595 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ {∅}𝐶 = 0)
7671, 75breqtrd 4837 . . . . . . . . 9 ((𝜑 ∧ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
77 simpr 477 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → ¬ ∃𝑘𝐴 𝐵 = ∅)
78 nfv 2009 . . . . . . . . . . . . 13 𝑦 ¬ ∃𝑘𝐴 𝐵 = ∅
7931nfn 1953 . . . . . . . . . . . . . . . . 17 𝑘 ¬ ∃𝑘𝐴 𝐵 = ∅
80 rabn0 4124 . . . . . . . . . . . . . . . . . . 19 ({𝑘𝐴𝐵 = ∅} ≠ ∅ ↔ ∃𝑘𝐴 𝐵 = ∅)
8180biimpi 207 . . . . . . . . . . . . . . . . . 18 ({𝑘𝐴𝐵 = ∅} ≠ ∅ → ∃𝑘𝐴 𝐵 = ∅)
8281necon1bi 2965 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → {𝑘𝐴𝐵 = ∅} = ∅)
83 eqid 2765 . . . . . . . . . . . . . . . . . 18 𝐵 = 𝐵
8483a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ∃𝑘𝐴 𝐵 = ∅ → 𝐵 = 𝐵)
8579, 82, 84mpteq12d 4895 . . . . . . . . . . . . . . . 16 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵))
86 mpt0 6201 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ∅ ↦ 𝐵) = ∅
8785, 86syl6eq 2815 . . . . . . . . . . . . . . 15 (¬ ∃𝑘𝐴 𝐵 = ∅ → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
8887rneqd 5523 . . . . . . . . . . . . . 14 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ran ∅)
89 rn0 5548 . . . . . . . . . . . . . 14 ran ∅ = ∅
9088, 89syl6eq 2815 . . . . . . . . . . . . 13 (¬ ∃𝑘𝐴 𝐵 = ∅ → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) = ∅)
9178, 90esumeq1d 30565 . . . . . . . . . . . 12 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = Σ*𝑦 ∈ ∅𝐶)
92 esumnul 30578 . . . . . . . . . . . 12 Σ*𝑦 ∈ ∅𝐶 = 0
9391, 92syl6eq 2815 . . . . . . . . . . 11 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
94 0le0 11384 . . . . . . . . . . 11 0 ≤ 0
9593, 94syl6eqbr 4850 . . . . . . . . . 10 (¬ ∃𝑘𝐴 𝐵 = ∅ → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9677, 95syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ ∃𝑘𝐴 𝐵 = ∅) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
9776, 96pm2.61dan 847 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0)
98 ssrab2 3849 . . . . . . . . . . . . 13 {𝑘𝐴𝐵 = ∅} ⊆ 𝐴
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → {𝑘𝐴𝐵 = ∅} ⊆ 𝐴)
1003, 99ssexd 4968 . . . . . . . . . . 11 (𝜑 → {𝑘𝐴𝐵 = ∅} ∈ V)
101 nfrab1 3270 . . . . . . . . . . . 12 𝑘{𝑘𝐴𝐵 = ∅}
102101mptexgf 6682 . . . . . . . . . . 11 ({𝑘𝐴𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
103 rnexg 7300 . . . . . . . . . . 11 ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
104100, 102, 1033syl 18 . . . . . . . . . 10 (𝜑 → ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V)
1052adantl 473 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
106 simplll 791 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
10799sselda 3763 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
108107adantlr 706 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝑘𝐴)
109108adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
110106, 109, 8syl2anc 579 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
111105, 110eqeltrd 2844 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
11254, 111, 66r19.29af 3223 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
113112ralrimiva 3113 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
114 nfcv 2907 . . . . . . . . . . 11 𝑦ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)
115114esumcl 30560 . . . . . . . . . 10 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∈ V ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞)) → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
116104, 113, 115syl2anc 579 . . . . . . . . 9 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞))
117 elxrge0 12490 . . . . . . . . . 10 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
118117simprbi 490 . . . . . . . . 9 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ (0[,]+∞) → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
119116, 118syl 17 . . . . . . . 8 (𝜑 → 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)
12097, 119jca 507 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶))
121 iccssxr 12463 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
122121, 116sseldi 3761 . . . . . . . 8 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
123121, 48sselii 3760 . . . . . . . . 9 0 ∈ ℝ*
124123a1i 11 . . . . . . . 8 (𝜑 → 0 ∈ ℝ*)
125 xrletri3 12192 . . . . . . . 8 ((Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* ∧ 0 ∈ ℝ*) → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
126122, 124, 125syl2anc 579 . . . . . . 7 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0 ↔ (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 ≤ 0 ∧ 0 ≤ Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶)))
127120, 126mpbird 248 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 = 0)
128127oveq1d 6861 . . . . 5 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
1299ralrimiva 3113 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1301esumcl 30560 . . . . . . . . 9 (({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V ∧ ∀𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞)) → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
1316, 129, 130syl2anc 579 . . . . . . . 8 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ (0[,]+∞))
132121, 131sseldi 3761 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ*)
13323, 132eqeltrd 2844 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ*)
134 xaddid2 12280 . . . . . 6 *𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶 ∈ ℝ* → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
135133, 134syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
136128, 135eqtrd 2799 . . . 4 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶)
137 simpl 474 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝜑)
13857adantl 473 . . . . . . . . . 10 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐵 = ∅)
139137, 107, 138, 42syl21anc 866 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 = 0)
140139ralrimiva 3113 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
14130, 140esumeq2d 30567 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0)
142101esum0 30579 . . . . . . . 8 ({𝑘𝐴𝐵 = ∅} ∈ V → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
143100, 142syl 17 . . . . . . 7 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}0 = 0)
144141, 143eqtrd 2799 . . . . . 6 (𝜑 → Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 = 0)
145144oveq1d 6861 . . . . 5 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
146 xaddid2 12280 . . . . . 6 *𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷 ∈ ℝ* → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
147132, 146syl 17 . . . . 5 (𝜑 → (0 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
148145, 147eqtrd 2799 . . . 4 (𝜑 → (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷) = Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷)
14923, 136, 1483eqtr4d 2809 . . 3 (𝜑 → (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶) = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
150 nfv 2009 . . . 4 𝑦𝜑
151 nfcv 2907 . . . 4 𝑦ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
1521mptexgf 6682 . . . . 5 ({𝑘𝐴 ∣ ¬ 𝐵 = ∅} ∈ V → (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
153 rnexg 7300 . . . . 5 ((𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
1546, 152, 1533syl 18 . . . 4 (𝜑 → ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∈ V)
15569ssrind 4001 . . . . . 6 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
156 incom 3969 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
15713neqned 2944 . . . . . . . . . . . 12 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → 𝐵 ≠ ∅)
158157necomd 2992 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ∅ ≠ 𝐵)
159158neneqd 2942 . . . . . . . . . 10 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} → ¬ ∅ = 𝐵)
160159nrex 3146 . . . . . . . . 9 ¬ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵
161 eqid 2765 . . . . . . . . . . 11 (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) = (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
162161elrnmpt 5543 . . . . . . . . . 10 (∅ ∈ V → (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵))
16372, 162ax-mp 5 . . . . . . . . 9 (∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}∅ = 𝐵)
164160, 163mtbir 314 . . . . . . . 8 ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
165 disjsn 4404 . . . . . . . 8 ((ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
166164, 165mpbir 222 . . . . . . 7 (ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ∩ {∅}) = ∅
167156, 166eqtr3i 2789 . . . . . 6 ({∅} ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅
168155, 167syl6sseq 3813 . . . . 5 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅)
169 ss0 4138 . . . . 5 ((ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ⊆ ∅ → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
170168, 169syl 17 . . . 4 (𝜑 → (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∩ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = ∅)
171 nfmpt1 4908 . . . . . . . 8 𝑘(𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
172171nfrn 5539 . . . . . . 7 𝑘ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17350, 172nfel 2920 . . . . . 6 𝑘 𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)
17430, 173nfan 1998 . . . . 5 𝑘(𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
1752adantl 473 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 = 𝐷)
176 simplll 791 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝜑)
1777adantlr 706 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) → 𝑘𝐴)
178177adantr 472 . . . . . . 7 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝑘𝐴)
179176, 178, 8syl2anc 579 . . . . . 6 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐷 ∈ (0[,]+∞))
180175, 179eqeltrd 2844 . . . . 5 ((((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) ∧ 𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ∧ 𝑦 = 𝐵) → 𝐶 ∈ (0[,]+∞))
181161elrnmpt 5543 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵))
18261, 181ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) ↔ ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
183182biimpi 207 . . . . . 6 (𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
184183adantl 473 . . . . 5 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → ∃𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝑦 = 𝐵)
185174, 180, 184r19.29af 3223 . . . 4 ((𝜑𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) → 𝐶 ∈ (0[,]+∞))
186150, 114, 151, 104, 154, 170, 112, 185esumsplit 30583 . . 3 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = (Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵)𝐶 +𝑒 Σ*𝑦 ∈ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)𝐶))
187 rabnc 4126 . . . . 5 ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅
188187a1i 11 . . . 4 (𝜑 → ({𝑘𝐴𝐵 = ∅} ∩ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) = ∅)
189107, 8syldan 585 . . . 4 ((𝜑𝑘 ∈ {𝑘𝐴𝐵 = ∅}) → 𝐷 ∈ (0[,]+∞))
19030, 101, 1, 100, 6, 188, 189, 9esumsplit 30583 . . 3 (𝜑 → Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷 = (Σ*𝑘 ∈ {𝑘𝐴𝐵 = ∅}𝐷 +𝑒 Σ*𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}𝐷))
191149, 186, 1903eqtr4d 2809 . 2 (𝜑 → Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
192 rabxm 4125 . . . . . . . 8 𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})
193192, 83mpteq12i 4903 . . . . . . 7 (𝑘𝐴𝐵) = (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵)
194 mptun 6205 . . . . . . 7 (𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}) ↦ 𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
195193, 194eqtri 2787 . . . . . 6 (𝑘𝐴𝐵) = ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
196195rneqi 5522 . . . . 5 ran (𝑘𝐴𝐵) = ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
197 rnun 5726 . . . . 5 ran ((𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
198196, 197eqtri 2787 . . . 4 ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))
199198a1i 11 . . 3 (𝜑 → ran (𝑘𝐴𝐵) = (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵)))
200150, 199esumeq1d 30565 . 2 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑦 ∈ (ran (𝑘 ∈ {𝑘𝐴𝐵 = ∅} ↦ 𝐵) ∪ ran (𝑘 ∈ {𝑘𝐴 ∣ ¬ 𝐵 = ∅} ↦ 𝐵))𝐶)
201192a1i 11 . . 3 (𝜑𝐴 = ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅}))
20230, 201esumeq1d 30565 . 2 (𝜑 → Σ*𝑘𝐴𝐷 = Σ*𝑘 ∈ ({𝑘𝐴𝐵 = ∅} ∪ {𝑘𝐴 ∣ ¬ 𝐵 = ∅})𝐷)
203191, 200, 2023eqtr4d 2809 1 (𝜑 → Σ*𝑦 ∈ ran (𝑘𝐴𝐵)𝐶 = Σ*𝑘𝐴𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cun 3732  cin 3733  wss 3734  c0 4081  {csn 4336  Disj wdisj 4779   class class class wbr 4811  cmpt 4890  ran crn 5280  (class class class)co 6846  0cc0 10193  +∞cpnf 10329  *cxr 10331  cle 10333   +𝑒 cxad 12149  [,]cicc 12385  Σ*cesum 30557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-disj 4780  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-fi 8528  df-sup 8559  df-inf 8560  df-oi 8626  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12386  df-ioc 12387  df-ico 12388  df-icc 12389  df-fz 12539  df-fzo 12679  df-fl 12806  df-mod 12882  df-seq 13014  df-exp 13073  df-fac 13270  df-bc 13299  df-hash 13327  df-shft 14106  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-limsup 14501  df-clim 14518  df-rlim 14519  df-sum 14716  df-ef 15094  df-sin 15096  df-cos 15097  df-pi 15099  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-starv 16243  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ple 16248  df-ds 16250  df-unif 16251  df-hom 16252  df-cco 16253  df-rest 16363  df-topn 16364  df-0g 16382  df-gsum 16383  df-topgen 16384  df-pt 16385  df-prds 16388  df-ordt 16441  df-xrs 16442  df-qtop 16447  df-imas 16448  df-xps 16450  df-mre 16526  df-mrc 16527  df-acs 16529  df-ps 17480  df-tsr 17481  df-plusf 17521  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-mhm 17615  df-submnd 17616  df-grp 17706  df-minusg 17707  df-sbg 17708  df-mulg 17822  df-subg 17869  df-cntz 18027  df-cmn 18475  df-abl 18476  df-mgp 18771  df-ur 18783  df-ring 18830  df-cring 18831  df-subrg 19061  df-abv 19100  df-lmod 19148  df-scaf 19149  df-sra 19460  df-rgmod 19461  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-fbas 20030  df-fg 20031  df-cnfld 20034  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-cld 21117  df-ntr 21118  df-cls 21119  df-nei 21196  df-lp 21234  df-perf 21235  df-cn 21325  df-cnp 21326  df-haus 21413  df-tx 21659  df-hmeo 21852  df-fil 21943  df-fm 22035  df-flim 22036  df-flf 22037  df-tmd 22169  df-tgp 22170  df-tsms 22223  df-trg 22256  df-xms 22418  df-ms 22419  df-tms 22420  df-nm 22680  df-ngp 22681  df-nrg 22683  df-nlm 22684  df-ii 22973  df-cncf 22974  df-limc 23935  df-dv 23936  df-log 24608  df-esum 30558
This theorem is referenced by:  carsggect  30848  carsgclctunlem2  30849  pmeasadd  30855
  Copyright terms: Public domain W3C validator