Definition df-xrs 17562

Description: The extended real number structure. Unlike df-cnfld 21388, 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 21388. 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 17560	. 2 class ℝ*𝑠
2		cnx 17240	. . . . . 6 class ndx
3		cbs 17258	. . . . . 6 class Base
4	2, 3	cfv 6573	. . . . 5 class (Base‘ndx)
5		cxr 11323	. . . . 5 class ℝ*
6	4, 5	cop 4654	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17311	. . . . . 6 class +g
8	2, 7	cfv 6573	. . . . 5 class (+g‘ndx)
9		cxad 13173	. . . . 5 class +𝑒
10	8, 9	cop 4654	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17312	. . . . . 6 class .r
12	2, 11	cfv 6573	. . . . 5 class (.r‘ndx)
13		cxmu 13174	. . . . 5 class ·e
14	12, 13	cop 4654	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4652	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17317	. . . . . 6 class TopSet
17	2, 16	cfv 6573	. . . . 5 class (TopSet‘ndx)
18		cle 11325	. . . . . 6 class ≤
19		cordt 17559	. . . . . 6 class ordTop
20	18, 19	cfv 6573	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4654	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17318	. . . . . 6 class le
23	2, 22	cfv 6573	. . . . 5 class (le‘ndx)
24	23, 18	cop 4654	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17320	. . . . . 6 class dist
26	2, 25	cfv 6573	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1536	. . . . . . . 8 class 𝑥
30	28	cv 1536	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5166	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13172	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7448	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13172	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7448	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4548	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7450	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4654	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4652	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3974	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1537	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21417  xrsex  21418  xrsbas  21419  xrsadd  21420  xrsmul  21421  xrstset  21422  xrsle  21423  xrsds  21450