Definition df-xrs 17534

Description: The extended real number structure. Unlike df-cnfld 21427, 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 21427. 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 17532	. 2 class ℝ*𝑠
2		cnx 17231	. . . . . 6 class ndx
3		cbs 17247	. . . . . 6 class Base
4	2, 3	cfv 6523	. . . . 5 class (Base‘ndx)
5		cxr 11217	. . . . 5 class ℝ*
6	4, 5	cop 4590	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17288	. . . . . 6 class +g
8	2, 7	cfv 6523	. . . . 5 class (+g‘ndx)
9		cxad 13114	. . . . 5 class +𝑒
10	8, 9	cop 4590	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17289	. . . . . 6 class .r
12	2, 11	cfv 6523	. . . . 5 class (.r‘ndx)
13		cxmu 13115	. . . . 5 class ·e
14	12, 13	cop 4590	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4588	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17294	. . . . . 6 class TopSet
17	2, 16	cfv 6523	. . . . 5 class (TopSet‘ndx)
18		cle 11219	. . . . . 6 class ≤
19		cordt 17531	. . . . . 6 class ordTop
20	18, 19	cfv 6523	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4590	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17295	. . . . . 6 class le
23	2, 22	cfv 6523	. . . . 5 class (le‘ndx)
24	23, 18	cop 4590	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17297	. . . . . 6 class dist
26	2, 25	cfv 6523	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1561	. . . . . . . 8 class 𝑥
30	28	cv 1561	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5102	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13113	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7398	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13113	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7398	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4482	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7400	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4590	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4588	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3904	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1562	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17636  xrsbas  17638  xrsstr  21442  xrsex  21443  xrsadd  21444  xrsmul  21445  xrstset  21446  xrsds  21464