Definition df-xrs 17403

Description: The extended real number structure. Unlike df-cnfld 21290, 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 21290. 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 17401	. 2 class ℝ*𝑠
2		cnx 17101	. . . . . 6 class ndx
3		cbs 17117	. . . . . 6 class Base
4	2, 3	cfv 6481	. . . . 5 class (Base‘ndx)
5		cxr 11142	. . . . 5 class ℝ*
6	4, 5	cop 4582	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17158	. . . . . 6 class +g
8	2, 7	cfv 6481	. . . . 5 class (+g‘ndx)
9		cxad 13006	. . . . 5 class +𝑒
10	8, 9	cop 4582	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17159	. . . . . 6 class .r
12	2, 11	cfv 6481	. . . . 5 class (.r‘ndx)
13		cxmu 13007	. . . . 5 class ·e
14	12, 13	cop 4582	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4580	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17164	. . . . . 6 class TopSet
17	2, 16	cfv 6481	. . . . 5 class (TopSet‘ndx)
18		cle 11144	. . . . . 6 class ≤
19		cordt 17400	. . . . . 6 class ordTop
20	18, 19	cfv 6481	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4582	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17165	. . . . . 6 class le
23	2, 22	cfv 6481	. . . . 5 class (le‘ndx)
24	23, 18	cop 4582	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17167	. . . . . 6 class dist
26	2, 25	cfv 6481	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1540	. . . . . . . 8 class 𝑥
30	28	cv 1540	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5091	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13005	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7346	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13005	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7346	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4475	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7348	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4582	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4580	. . 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 1541	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17505  xrsbas  17507  xrsstr  21318  xrsex  21319  xrsadd  21320  xrsmul  21321  xrstset  21322  xrsds  21344