Definition df-xrs 17509

Description: The extended real number structure. Unlike df-cnfld 21337, 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 21337. 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 17507	. 2 class ℝ*𝑠
2		cnx 17187	. . . . . 6 class ndx
3		cbs 17205	. . . . . 6 class Base
4	2, 3	cfv 6543	. . . . 5 class (Base‘ndx)
5		cxr 11285	. . . . 5 class ℝ*
6	4, 5	cop 4629	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17258	. . . . . 6 class +g
8	2, 7	cfv 6543	. . . . 5 class (+g‘ndx)
9		cxad 13135	. . . . 5 class +𝑒
10	8, 9	cop 4629	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17259	. . . . . 6 class .r
12	2, 11	cfv 6543	. . . . 5 class (.r‘ndx)
13		cxmu 13136	. . . . 5 class ·e
14	12, 13	cop 4629	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4627	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17264	. . . . . 6 class TopSet
17	2, 16	cfv 6543	. . . . 5 class (TopSet‘ndx)
18		cle 11287	. . . . . 6 class ≤
19		cordt 17506	. . . . . 6 class ordTop
20	18, 19	cfv 6543	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4629	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17265	. . . . . 6 class le
23	2, 22	cfv 6543	. . . . 5 class (le‘ndx)
24	23, 18	cop 4629	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17267	. . . . . 6 class dist
26	2, 25	cfv 6543	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1533	. . . . . . . 8 class 𝑥
30	28	cv 1533	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5143	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13134	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7413	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13134	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7413	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4523	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7415	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4629	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4627	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3944	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1534	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21366  xrsex  21367  xrsbas  21368  xrsadd  21369  xrsmul  21370  xrstset  21371  xrsle  21372  xrsds  21399