Definition df-xrs 17465

Description: The extended real number structure. Unlike df-cnfld 21265, 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 21265. 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 17463	. 2 class ℝ*𝑠
2		cnx 17163	. . . . . 6 class ndx
3		cbs 17179	. . . . . 6 class Base
4	2, 3	cfv 6511	. . . . 5 class (Base‘ndx)
5		cxr 11207	. . . . 5 class ℝ*
6	4, 5	cop 4595	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17220	. . . . . 6 class +g
8	2, 7	cfv 6511	. . . . 5 class (+g‘ndx)
9		cxad 13070	. . . . 5 class +𝑒
10	8, 9	cop 4595	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17221	. . . . . 6 class .r
12	2, 11	cfv 6511	. . . . 5 class (.r‘ndx)
13		cxmu 13071	. . . . 5 class ·e
14	12, 13	cop 4595	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4593	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17226	. . . . . 6 class TopSet
17	2, 16	cfv 6511	. . . . 5 class (TopSet‘ndx)
18		cle 11209	. . . . . 6 class ≤
19		cordt 17462	. . . . . 6 class ordTop
20	18, 19	cfv 6511	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4595	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17227	. . . . . 6 class le
23	2, 22	cfv 6511	. . . . 5 class (le‘ndx)
24	23, 18	cop 4595	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17229	. . . . . 6 class dist
26	2, 25	cfv 6511	. . . . 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 5107	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13069	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7387	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13069	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7387	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4488	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7389	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4595	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4593	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3912	. 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  21293  xrsex  21294  xrsbas  21295  xrsadd  21296  xrsmul  21297  xrstset  21298  xrsle  21299  xrsds  21326