Definition df-xrs 17424

Description: The extended real number structure. Unlike df-cnfld 21280, 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 21280. 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 17422	. 2 class ℝ*𝑠
2		cnx 17122	. . . . . 6 class ndx
3		cbs 17138	. . . . . 6 class Base
4	2, 3	cfv 6486	. . . . 5 class (Base‘ndx)
5		cxr 11167	. . . . 5 class ℝ*
6	4, 5	cop 4585	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17179	. . . . . 6 class +g
8	2, 7	cfv 6486	. . . . 5 class (+g‘ndx)
9		cxad 13030	. . . . 5 class +𝑒
10	8, 9	cop 4585	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17180	. . . . . 6 class .r
12	2, 11	cfv 6486	. . . . 5 class (.r‘ndx)
13		cxmu 13031	. . . . 5 class ·e
14	12, 13	cop 4585	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4583	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17185	. . . . . 6 class TopSet
17	2, 16	cfv 6486	. . . . 5 class (TopSet‘ndx)
18		cle 11169	. . . . . 6 class ≤
19		cordt 17421	. . . . . 6 class ordTop
20	18, 19	cfv 6486	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4585	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17186	. . . . . 6 class le
23	2, 22	cfv 6486	. . . . 5 class (le‘ndx)
24	23, 18	cop 4585	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17188	. . . . . 6 class dist
26	2, 25	cfv 6486	. . . . 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 5095	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13029	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7353	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13029	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7353	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4478	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7355	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4585	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4583	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3903	. 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:  xrsle  17526  xrsbas  17528  xrsstr  21308  xrsex  21309  xrsadd  21310  xrsmul  21311  xrstset  21312  xrsds  21334