Definition df-xrs 17425

Description: The extended real number structure. Unlike df-cnfld 21312, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 21312. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because +∞ is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +∞ an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with ℂ_fld when restricted to ℝ. (Contributed by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
df-xrs	⊢ ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-xrs

Step	Hyp	Ref	Expression
1		cxrs 17423	. 2 class ℝ*𝑠
2		cnx 17122	. . . . . 6 class ndx
3		cbs 17138	. . . . . 6 class Base
4	2, 3	cfv 6492	. . . . 5 class (Base‘ndx)
5		cxr 11167	. . . . 5 class ℝ*
6	4, 5	cop 4586	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17179	. . . . . 6 class +g
8	2, 7	cfv 6492	. . . . 5 class (+g‘ndx)
9		cxad 13026	. . . . 5 class +𝑒
10	8, 9	cop 4586	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17180	. . . . . 6 class .r
12	2, 11	cfv 6492	. . . . 5 class (.r‘ndx)
13		cxmu 13027	. . . . 5 class ·e
14	12, 13	cop 4586	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4584	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17185	. . . . . 6 class TopSet
17	2, 16	cfv 6492	. . . . 5 class (TopSet‘ndx)
18		cle 11169	. . . . . 6 class ≤
19		cordt 17422	. . . . . 6 class ordTop
20	18, 19	cfv 6492	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4586	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17186	. . . . . 6 class le
23	2, 22	cfv 6492	. . . . 5 class (le‘ndx)
24	23, 18	cop 4586	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17188	. . . . . 6 class dist
26	2, 25	cfv 6492	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1540	. . . . . . . 8 class 𝑥
30	28	cv 1540	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5098	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13025	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7358	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13025	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7358	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4479	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7360	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4586	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4584	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3899	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1541	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17527  xrsbas  17529  xrsstr  21340  xrsex  21341  xrsadd  21342  xrsmul  21343  xrstset  21344  xrsds  21366