Definition df-xrs 17471

Description: The extended real number structure. Unlike df-cnfld 21271, 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 21271. 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 17469	. 2 class ℝ*𝑠
2		cnx 17169	. . . . . 6 class ndx
3		cbs 17185	. . . . . 6 class Base
4	2, 3	cfv 6513	. . . . 5 class (Base‘ndx)
5		cxr 11213	. . . . 5 class ℝ*
6	4, 5	cop 4597	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17226	. . . . . 6 class +g
8	2, 7	cfv 6513	. . . . 5 class (+g‘ndx)
9		cxad 13076	. . . . 5 class +𝑒
10	8, 9	cop 4597	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17227	. . . . . 6 class .r
12	2, 11	cfv 6513	. . . . 5 class (.r‘ndx)
13		cxmu 13077	. . . . 5 class ·e
14	12, 13	cop 4597	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4595	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17232	. . . . . 6 class TopSet
17	2, 16	cfv 6513	. . . . 5 class (TopSet‘ndx)
18		cle 11215	. . . . . 6 class ≤
19		cordt 17468	. . . . . 6 class ordTop
20	18, 19	cfv 6513	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4597	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17233	. . . . . 6 class le
23	2, 22	cfv 6513	. . . . 5 class (le‘ndx)
24	23, 18	cop 4597	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17235	. . . . . 6 class dist
26	2, 25	cfv 6513	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1539	. . . . . . . 8 class 𝑥
30	28	cv 1539	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5109	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13075	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7389	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13075	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7389	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4490	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7391	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4597	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4595	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3914	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1540	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21299  xrsex  21300  xrsbas  21301  xrsadd  21302  xrsmul  21303  xrstset  21304  xrsle  21305  xrsds  21332