Definition df-xrs 16370

Description: The extended real number structure. Unlike df-cnfld 19958, 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 19958. 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 16368	. 2 class ℝ*𝑠
2		cnx 16068	. . . . . 6 class ndx
3		cbs 16071	. . . . . 6 class Base
4	2, 3	cfv 6104	. . . . 5 class (Base‘ndx)
5		cxr 10361	. . . . 5 class ℝ*
6	4, 5	cop 4383	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16156	. . . . . 6 class +g
8	2, 7	cfv 6104	. . . . 5 class (+g‘ndx)
9		cxad 12163	. . . . 5 class +𝑒
10	8, 9	cop 4383	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16157	. . . . . 6 class .r
12	2, 11	cfv 6104	. . . . 5 class (.r‘ndx)
13		cxmu 12164	. . . . 5 class ·e
14	12, 13	cop 4383	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4381	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16162	. . . . . 6 class TopSet
17	2, 16	cfv 6104	. . . . 5 class (TopSet‘ndx)
18		cle 10363	. . . . . 6 class ≤
19		cordt 16367	. . . . . 6 class ordTop
20	18, 19	cfv 6104	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4383	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16163	. . . . . 6 class le
23	2, 22	cfv 6104	. . . . 5 class (le‘ndx)
24	23, 18	cop 4383	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16165	. . . . . 6 class dist
26	2, 25	cfv 6104	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1636	. . . . . . . 8 class 𝑥
30	28	cv 1636	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 4851	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12162	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 6877	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12162	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 6877	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4286	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpt2 6879	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4383	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4381	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3774	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1637	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  19971  xrsex  19972  xrsbas  19973  xrsadd  19974  xrsmul  19975  xrstset  19976  xrsle  19977  xrsds  20000