Definition df-xrs 17463

Description: The extended real number structure. Unlike df-cnfld 21350, 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 21350. 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 17461	. 2 class ℝ*𝑠
2		cnx 17160	. . . . . 6 class ndx
3		cbs 17176	. . . . . 6 class Base
4	2, 3	cfv 6496	. . . . 5 class (Base‘ndx)
5		cxr 11175	. . . . 5 class ℝ*
6	4, 5	cop 4574	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17217	. . . . . 6 class +g
8	2, 7	cfv 6496	. . . . 5 class (+g‘ndx)
9		cxad 13058	. . . . 5 class +𝑒
10	8, 9	cop 4574	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17218	. . . . . 6 class .r
12	2, 11	cfv 6496	. . . . 5 class (.r‘ndx)
13		cxmu 13059	. . . . 5 class ·e
14	12, 13	cop 4574	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4572	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17223	. . . . . 6 class TopSet
17	2, 16	cfv 6496	. . . . 5 class (TopSet‘ndx)
18		cle 11177	. . . . . 6 class ≤
19		cordt 17460	. . . . . 6 class ordTop
20	18, 19	cfv 6496	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4574	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17224	. . . . . 6 class le
23	2, 22	cfv 6496	. . . . 5 class (le‘ndx)
24	23, 18	cop 4574	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17226	. . . . . 6 class dist
26	2, 25	cfv 6496	. . . . 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 5086	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13057	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7364	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13057	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7364	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4467	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7366	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4574	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4572	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3888	. 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  17565  xrsbas  17567  xrsstr  21365  xrsex  21366  xrsadd  21367  xrsmul  21368  xrstset  21369  xrsds  21387