Definition df-xrs 16162

Description: The extended real number structure. Unlike df-cnfld 19747, 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 19747. 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 16160	. 2 class ℝ*𝑠
2		cnx 15854	. . . . . 6 class ndx
3		cbs 15857	. . . . . 6 class Base
4	2, 3	cfv 5888	. . . . 5 class (Base‘ndx)
5		cxr 10073	. . . . 5 class ℝ*
6	4, 5	cop 4183	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 15941	. . . . . 6 class +g
8	2, 7	cfv 5888	. . . . 5 class (+g‘ndx)
9		cxad 11944	. . . . 5 class +𝑒
10	8, 9	cop 4183	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 15942	. . . . . 6 class .r
12	2, 11	cfv 5888	. . . . 5 class (.r‘ndx)
13		cxmu 11945	. . . . 5 class ·e
14	12, 13	cop 4183	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4181	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 15947	. . . . . 6 class TopSet
17	2, 16	cfv 5888	. . . . 5 class (TopSet‘ndx)
18		cle 10075	. . . . . 6 class ≤
19		cordt 16159	. . . . . 6 class ordTop
20	18, 19	cfv 5888	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4183	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 15948	. . . . . 6 class le
23	2, 22	cfv 5888	. . . . 5 class (le‘ndx)
24	23, 18	cop 4183	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 15950	. . . . . 6 class dist
26	2, 25	cfv 5888	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1482	. . . . . . . 8 class 𝑥
30	28	cv 1482	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 4653	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 11943	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 6650	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 11943	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 6650	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4086	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpt2 6652	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4183	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4181	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3572	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1483	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  19760  xrsex  19761  xrsbas  19762  xrsadd  19763  xrsmul  19764  xrstset  19765  xrsle  19766  xrsds  19789