Definition df-xrs 17437

Description: The extended real number structure. Unlike df-cnfld 21327, 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 21327. 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 17435	. 2 class ℝ*𝑠
2		cnx 17134	. . . . . 6 class ndx
3		cbs 17150	. . . . . 6 class Base
4	2, 3	cfv 6502	. . . . 5 class (Base‘ndx)
5		cxr 11179	. . . . 5 class ℝ*
6	4, 5	cop 4588	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17191	. . . . . 6 class +g
8	2, 7	cfv 6502	. . . . 5 class (+g‘ndx)
9		cxad 13038	. . . . 5 class +𝑒
10	8, 9	cop 4588	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17192	. . . . . 6 class .r
12	2, 11	cfv 6502	. . . . 5 class (.r‘ndx)
13		cxmu 13039	. . . . 5 class ·e
14	12, 13	cop 4588	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4586	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17197	. . . . . 6 class TopSet
17	2, 16	cfv 6502	. . . . 5 class (TopSet‘ndx)
18		cle 11181	. . . . . 6 class ≤
19		cordt 17434	. . . . . 6 class ordTop
20	18, 19	cfv 6502	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4588	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17198	. . . . . 6 class le
23	2, 22	cfv 6502	. . . . 5 class (le‘ndx)
24	23, 18	cop 4588	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17200	. . . . . 6 class dist
26	2, 25	cfv 6502	. . . . 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 5100	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13037	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7370	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13037	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7370	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4481	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7372	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4588	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4586	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3901	. 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  17539  xrsbas  17541  xrsstr  21355  xrsex  21356  xrsadd  21357  xrsmul  21358  xrstset  21359  xrsds  21381