Definition df-xrs 17674

Description: The extended real number structure. Unlike df-cnfld 21679, 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 21679. 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), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-xrs

Step	Hyp	Ref	Expression
1		cxrs 17672	. 2 class ℝ*𝑠
2		cnx 17371	. . . . . 6 class ndx
3		cbs 17387	. . . . . 6 class Base
4	2, 3	cfv 6538	. . . . 5 class (Base‘ndx)
5		cxr 11342	. . . . 5 class ℝ*
6	4, 5	cop 4589	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17428	. . . . . 6 class +g
8	2, 7	cfv 6538	. . . . 5 class (+g‘ndx)
9		cxad 13239	. . . . 5 class +e
10	8, 9	cop 4589	. . . 4 class ⟨(+g‘ndx), +e ⟩
11		cmulr 17429	. . . . . 6 class .r
12	2, 11	cfv 6538	. . . . 5 class (.r‘ndx)
13		cxmu 13240	. . . . 5 class ·e
14	12, 13	cop 4589	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4587	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17434	. . . . . 6 class TopSet
17	2, 16	cfv 6538	. . . . 5 class (TopSet‘ndx)
18		cle 11344	. . . . . 6 class ≤
19		cordt 17671	. . . . . 6 class ordTop
20	18, 19	cfv 6538	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4589	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17435	. . . . . 6 class le
23	2, 22	cfv 6538	. . . . 5 class (le‘ndx)
24	23, 18	cop 4589	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17437	. . . . . 6 class dist
26	2, 25	cfv 6538	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1568	. . . . . . . 8 class 𝑥
30	28	cv 1568	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5102	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13238	. . . . . . . 8 class -e𝑥
33	30, 32, 9	co 7420	. . . . . . 7 class (𝑦 +e -e𝑥)
34	30	cxne 13238	. . . . . . . 8 class -e𝑦
35	29, 34, 9	co 7420	. . . . . . 7 class (𝑥 +e -e𝑦)
36	31, 33, 35	cif 4481	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦))
37	27, 28, 5, 5, 36	cmpo 7422	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))
38	26, 37	cop 4589	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩
39	21, 24, 38	ctp 4587	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩}
40	15, 39	cun 4149	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})
41	1, 40	wceq 1569	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})

This definition is used by:  xrsle  17776  xrsbas  17778  xrsstr  21694  xrsex  21695  xrsadd  21696  xrsmul  21697  xrstset  21698  xrsds  21716