Definition df-xrs 16775

Description: The extended real number structure. Unlike df-cnfld 20546, 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 20546. 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 16773	. 2 class ℝ*𝑠
2		cnx 16480	. . . . . 6 class ndx
3		cbs 16483	. . . . . 6 class Base
4	2, 3	cfv 6355	. . . . 5 class (Base‘ndx)
5		cxr 10674	. . . . 5 class ℝ*
6	4, 5	cop 4573	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16565	. . . . . 6 class +g
8	2, 7	cfv 6355	. . . . 5 class (+g‘ndx)
9		cxad 12506	. . . . 5 class +𝑒
10	8, 9	cop 4573	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16566	. . . . . 6 class .r
12	2, 11	cfv 6355	. . . . 5 class (.r‘ndx)
13		cxmu 12507	. . . . 5 class ·e
14	12, 13	cop 4573	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4571	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16571	. . . . . 6 class TopSet
17	2, 16	cfv 6355	. . . . 5 class (TopSet‘ndx)
18		cle 10676	. . . . . 6 class ≤
19		cordt 16772	. . . . . 6 class ordTop
20	18, 19	cfv 6355	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4573	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16572	. . . . . 6 class le
23	2, 22	cfv 6355	. . . . 5 class (le‘ndx)
24	23, 18	cop 4573	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16574	. . . . . 6 class dist
26	2, 25	cfv 6355	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1536	. . . . . . . 8 class 𝑥
30	28	cv 1536	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5066	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12505	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7156	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12505	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7156	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4467	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7158	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4573	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4571	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3934	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1537	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20559  xrsex  20560  xrsbas  20561  xrsadd  20562  xrsmul  20563  xrstset  20564  xrsle  20565  xrsds  20588