Definition df-xrs 17452

Description: The extended real number structure. Unlike df-cnfld 21145, 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 21145. 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 17450	. 2 class ℝ*𝑠
2		cnx 17130	. . . . . 6 class ndx
3		cbs 17148	. . . . . 6 class Base
4	2, 3	cfv 6543	. . . . 5 class (Base‘ndx)
5		cxr 11251	. . . . 5 class ℝ*
6	4, 5	cop 4634	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17201	. . . . . 6 class +g
8	2, 7	cfv 6543	. . . . 5 class (+g‘ndx)
9		cxad 13094	. . . . 5 class +𝑒
10	8, 9	cop 4634	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17202	. . . . . 6 class .r
12	2, 11	cfv 6543	. . . . 5 class (.r‘ndx)
13		cxmu 13095	. . . . 5 class ·e
14	12, 13	cop 4634	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4632	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17207	. . . . . 6 class TopSet
17	2, 16	cfv 6543	. . . . 5 class (TopSet‘ndx)
18		cle 11253	. . . . . 6 class ≤
19		cordt 17449	. . . . . 6 class ordTop
20	18, 19	cfv 6543	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4634	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17208	. . . . . 6 class le
23	2, 22	cfv 6543	. . . . 5 class (le‘ndx)
24	23, 18	cop 4634	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17210	. . . . . 6 class dist
26	2, 25	cfv 6543	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1540	. . . . . . . 8 class 𝑥
30	28	cv 1540	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5148	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13093	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7411	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13093	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7411	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4528	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7413	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4634	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4632	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3946	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1541	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21159  xrsex  21160  xrsbas  21161  xrsadd  21162  xrsmul  21163  xrstset  21164  xrsle  21165  xrsds  21188