Definition df-xrs 17455

Description: The extended real number structure. Unlike df-cnfld 21342, 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 21342. 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 17453	. 2 class ℝ*𝑠
2		cnx 17152	. . . . . 6 class ndx
3		cbs 17168	. . . . . 6 class Base
4	2, 3	cfv 6487	. . . . 5 class (Base‘ndx)
5		cxr 11167	. . . . 5 class ℝ*
6	4, 5	cop 4563	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17209	. . . . . 6 class +g
8	2, 7	cfv 6487	. . . . 5 class (+g‘ndx)
9		cxad 13050	. . . . 5 class +𝑒
10	8, 9	cop 4563	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17210	. . . . . 6 class .r
12	2, 11	cfv 6487	. . . . 5 class (.r‘ndx)
13		cxmu 13051	. . . . 5 class ·e
14	12, 13	cop 4563	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4561	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17215	. . . . . 6 class TopSet
17	2, 16	cfv 6487	. . . . 5 class (TopSet‘ndx)
18		cle 11169	. . . . . 6 class ≤
19		cordt 17452	. . . . . 6 class ordTop
20	18, 19	cfv 6487	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4563	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17216	. . . . . 6 class le
23	2, 22	cfv 6487	. . . . 5 class (le‘ndx)
24	23, 18	cop 4563	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17218	. . . . . 6 class dist
26	2, 25	cfv 6487	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1541	. . . . . . . 8 class 𝑥
30	28	cv 1541	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5074	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13049	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7356	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13049	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7356	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4456	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7358	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4563	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4561	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3883	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1542	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17557  xrsbas  17559  xrsstr  21357  xrsex  21358  xrsadd  21359  xrsmul  21360  xrstset  21361  xrsds  21379