Definition df-xrs 17130

Description: The extended real number structure. Unlike df-cnfld 20511, 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 20511. 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 17128	. 2 class ℝ*𝑠
2		cnx 16822	. . . . . 6 class ndx
3		cbs 16840	. . . . . 6 class Base
4	2, 3	cfv 6418	. . . . 5 class (Base‘ndx)
5		cxr 10939	. . . . 5 class ℝ*
6	4, 5	cop 4564	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16888	. . . . . 6 class +g
8	2, 7	cfv 6418	. . . . 5 class (+g‘ndx)
9		cxad 12775	. . . . 5 class +𝑒
10	8, 9	cop 4564	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16889	. . . . . 6 class .r
12	2, 11	cfv 6418	. . . . 5 class (.r‘ndx)
13		cxmu 12776	. . . . 5 class ·e
14	12, 13	cop 4564	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4562	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16894	. . . . . 6 class TopSet
17	2, 16	cfv 6418	. . . . 5 class (TopSet‘ndx)
18		cle 10941	. . . . . 6 class ≤
19		cordt 17127	. . . . . 6 class ordTop
20	18, 19	cfv 6418	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4564	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16895	. . . . . 6 class le
23	2, 22	cfv 6418	. . . . 5 class (le‘ndx)
24	23, 18	cop 4564	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16897	. . . . . 6 class dist
26	2, 25	cfv 6418	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1538	. . . . . . . 8 class 𝑥
30	28	cv 1538	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5070	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12774	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7255	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12774	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7255	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4456	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7257	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4564	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4562	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3881	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1539	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20524  xrsex  20525  xrsbas  20526  xrsadd  20527  xrsmul  20528  xrstset  20529  xrsle  20530  xrsds  20553