Definition df-xrs 17592

Description: The extended real number structure. Unlike df-cnfld 21587, 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 21587. 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 17590	. 2 class ℝ*𝑠
2		cnx 17289	. . . . . 6 class ndx
3		cbs 17305	. . . . . 6 class Base
4	2, 3	cfv 6537	. . . . 5 class (Base‘ndx)
5		cxr 11269	. . . . 5 class ℝ*
6	4, 5	cop 4593	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17346	. . . . . 6 class +g
8	2, 7	cfv 6537	. . . . 5 class (+g‘ndx)
9		cxad 13163	. . . . 5 class +𝑒
10	8, 9	cop 4593	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17347	. . . . . 6 class .r
12	2, 11	cfv 6537	. . . . 5 class (.r‘ndx)
13		cxmu 13164	. . . . 5 class ·e
14	12, 13	cop 4593	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4591	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17352	. . . . . 6 class TopSet
17	2, 16	cfv 6537	. . . . 5 class (TopSet‘ndx)
18		cle 11271	. . . . . 6 class ≤
19		cordt 17589	. . . . . 6 class ordTop
20	18, 19	cfv 6537	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4593	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17353	. . . . . 6 class le
23	2, 22	cfv 6537	. . . . 5 class (le‘ndx)
24	23, 18	cop 4593	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17355	. . . . . 6 class dist
26	2, 25	cfv 6537	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1569	. . . . . . . 8 class 𝑥
30	28	cv 1569	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5107	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13162	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7416	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13162	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7416	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4485	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7418	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4593	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4591	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3900	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1570	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is used by:  xrsle  17694  xrsbas  17696  xrsstr  21602  xrsex  21603  xrsadd  21604  xrsmul  21605  xrstset  21606  xrsds  21624