Metamath Proof Explorer

Theorem redvmptabs

Description: The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025)

Ref Expression
Hypothesis redvabs.d ⊢ 𝐷 = ( ℝ ∖ { 0 } )
Assertion redvmptabs ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) )

Proof

Step Hyp Ref Expression
1 redvabs.d ⊢ 𝐷 = ( ℝ ∖ { 0 } )
2 partfun ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) )
3 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
4 3 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
5 inss1 ⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ 𝐷
6 difss ⊢ ( ℝ ∖ { 0 } ) ⊆ ℝ
7 1 6 eqsstri ⊢ 𝐷 ⊆ ℝ
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 7 8 sstri ⊢ 𝐷 ⊆ ℂ
10 5 9 sstri ⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ
11 10 sseli ⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 ∈ ℂ )
12 11 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → 𝑥 ∈ ℂ )
13 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → 1 ∈ ℂ )
14 8 a1i ⊢ ( ⊤ → ℝ ⊆ ℂ )
15 14 sselda ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
16 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
17 4 dvmptid ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
18 ssinss1 ⊢ ( 𝐷 ⊆ ℝ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ )
19 7 18 mp1i ⊢ ( ⊤ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ )
20 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21 20 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
22 1 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( ℝ ∖ { 0 } ) )
23 eldifsn ⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
24 22 23 bitri ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
25 vex ⊢ 𝑥 ∈ V
26 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 < 0 ↔ 𝑥 < 0 ) )
27 25 26 elab ⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ↔ 𝑥 < 0 )
28 24 27 anbi12i ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) )
29 lt0ne0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) → 𝑥 ≠ 0 )
30 29 expcom ⊢ ( 𝑥 < 0 → ( 𝑥 ∈ ℝ → 𝑥 ≠ 0 ) )
31 30 pm4.71d ⊢ ( 𝑥 < 0 → ( 𝑥 ∈ ℝ ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ) )
32 31 bicomd ⊢ ( 𝑥 < 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ↔ 𝑥 ∈ ℝ ) )
33 32 pm5.32ri ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) )
34 28 33 bitri ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) )
35 elin ⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) )
36 0xr ⊢ 0 ∈ ℝ*
37 elioomnf ⊢ ( 0 ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) )
38 36 37 ax-mp ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) )
39 34 35 38 3bitr4i ⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↔ 𝑥 ∈ ( -∞ (,) 0 ) )
40 39 eqriv ⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) = ( -∞ (,) 0 )
41 iooretop ⊢ ( -∞ (,) 0 ) ∈ ( topGen ‘ ran (,) )
42 40 41 eqeltri ⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) )
43 42 a1i ⊢ ( ⊤ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) )
44 4 15 16 17 19 21 20 43 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) )
45 4 12 13 44 dvmptneg ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) )
46 45 mptru ⊢ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 )
47 7 a1i ⊢ ( ⊤ → 𝐷 ⊆ ℝ )
48 47 ssdifssd ⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ )
49 27 notbii ⊢ ( ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ↔ ¬ 𝑥 < 0 )
50 24 49 anbi12i ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) )
51 anass ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ) )
52 elre0re ⊢ ( 𝑥 ∈ ℝ → 0 ∈ ℝ )
53 id ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
54 52 53 lttrid ⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 ↔ ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ) )
55 ioran ⊢ ( ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ↔ ( ¬ 0 = 𝑥 ∧ ¬ 𝑥 < 0 ) )
56 nesym ⊢ ( 𝑥 ≠ 0 ↔ ¬ 0 = 𝑥 )
57 56 bicomi ⊢ ( ¬ 0 = 𝑥 ↔ 𝑥 ≠ 0 )
58 55 57 bianbi ⊢ ( ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ↔ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) )
59 54 58 bitr2di ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ↔ 0 < 𝑥 ) )
60 59 pm5.32i ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
61 50 51 60 3bitri ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
62 eldif ⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) )
63 repos ⊢ ( 𝑥 ∈ ( 0 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
64 61 62 63 3bitr4i ⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↔ 𝑥 ∈ ( 0 (,) +∞ ) )
65 64 eqriv ⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) = ( 0 (,) +∞ )
66 iooretop ⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
67 65 66 eqeltri ⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) )
68 67 a1i ⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) )
69 4 15 16 17 48 21 20 68 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) )
70 69 mptru ⊢ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 )
71 46 70 uneq12i ⊢ ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) )
72 12 negcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → - 𝑥 ∈ ℂ )
73 72 fmpttd ⊢ ( ⊤ → ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) : ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⟶ ℂ )
74 ssdifss ⊢ ( 𝐷 ⊆ ℝ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ )
75 7 74 ax-mp ⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ
76 75 8 sstri ⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ
77 76 a1i ⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ )
78 77 sselda ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) → 𝑥 ∈ ℂ )
79 78 fmpttd ⊢ ( ⊤ → ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) : ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⟶ ℂ )
80 inindif ⊢ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∩ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ∅
81 80 a1i ⊢ ( ⊤ → ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∩ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ∅ )
82 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
83 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) )
84 82 42 83 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } )
85 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) )
86 82 67 85 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } )
87 84 86 uneq12i ⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) )
88 unopn ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ∧ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) ) )
89 82 42 67 88 mp3an ⊢ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) )
90 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) )
91 82 89 90 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) )
92 87 91 eqtr4i ⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) )
93 92 a1i ⊢ ( ⊤ → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) )
94 21 20 14 73 79 19 48 81 93 dvun ⊢ ( ⊤ → ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) )
95 94 mptru ⊢ ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) )
96 2 71 95 3eqtr2ri ⊢ ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) )
97 partfun ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) )
98 elioore ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 ∈ ℝ )
99 0red ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 0 ∈ ℝ )
100 38 simprbi ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 < 0 )
101 98 99 100 ltled ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 ≤ 0 )
102 98 101 absnidd ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → ( abs ‘ 𝑥 ) = - 𝑥 )
103 102 eqcomd ⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → - 𝑥 = ( abs ‘ 𝑥 ) )
104 103 40 eleq2s ⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) → - 𝑥 = ( abs ‘ 𝑥 ) )
105 35 104 sylbir ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) → - 𝑥 = ( abs ‘ 𝑥 ) )
106 rpabsid ⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ 𝑥 ) = 𝑥 )
107 106 eqcomd ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 = ( abs ‘ 𝑥 ) )
108 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
109 107 108 eleq2s ⊢ ( 𝑥 ∈ ( 0 (,) +∞ ) → 𝑥 = ( abs ‘ 𝑥 ) )
110 109 65 eleq2s ⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 = ( abs ‘ 𝑥 ) )
111 62 110 sylbir ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 = ( abs ‘ 𝑥 ) )
112 105 111 ifeqda ⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) = ( abs ‘ 𝑥 ) )
113 112 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) )
114 97 113 eqtr3i ⊢ ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) )
115 114 oveq2i ⊢ ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) )
116 eqid ⊢ 1 = 1
117 27 116 ifbieq2i ⊢ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) = if ( 𝑥 < 0 , - 1 , 1 )
118 117 mpteq2i ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) )
119 96 115 118 3eqtr3i ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) )