Definition df-xrs 17547

Description: The extended real number structure. Unlike df-cnfld 21365, 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 21365. 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 17545	. 2 class ℝ*𝑠
2		cnx 17230	. . . . . 6 class ndx
3		cbs 17247	. . . . . 6 class Base
4	2, 3	cfv 6561	. . . . 5 class (Base‘ndx)
5		cxr 11294	. . . . 5 class ℝ*
6	4, 5	cop 4632	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17297	. . . . . 6 class +g
8	2, 7	cfv 6561	. . . . 5 class (+g‘ndx)
9		cxad 13152	. . . . 5 class +𝑒
10	8, 9	cop 4632	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17298	. . . . . 6 class .r
12	2, 11	cfv 6561	. . . . 5 class (.r‘ndx)
13		cxmu 13153	. . . . 5 class ·e
14	12, 13	cop 4632	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4630	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17303	. . . . . 6 class TopSet
17	2, 16	cfv 6561	. . . . 5 class (TopSet‘ndx)
18		cle 11296	. . . . . 6 class ≤
19		cordt 17544	. . . . . 6 class ordTop
20	18, 19	cfv 6561	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4632	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17304	. . . . . 6 class le
23	2, 22	cfv 6561	. . . . 5 class (le‘ndx)
24	23, 18	cop 4632	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17306	. . . . . 6 class dist
26	2, 25	cfv 6561	. . . . 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 5143	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13151	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7431	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13151	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7431	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4525	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7433	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4632	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4630	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3949	. 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  21394  xrsex  21395  xrsbas  21396  xrsadd  21397  xrsmul  21398  xrstset  21399  xrsle  21400  xrsds  21427