Definition df-xrs 17700

Description: The extended real number structure. Unlike df-cnfld 21706, 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 21706. 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), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-xrs

Step	Hyp	Ref	Expression
1		cxrs 17698	. 2 class ℝ*𝑠
2		cnx 17397	. . . . . 6 class ndx
3		cbs 17413	. . . . . 6 class Base
4	2, 3	cfv 6555	. . . . 5 class (Base‘ndx)
5		cxr 11366	. . . . 5 class ℝ*
6	4, 5	cop 4838	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17454	. . . . . 6 class +g
8	2, 7	cfv 6555	. . . . 5 class (+g‘ndx)
9		cxad 13263	. . . . 5 class +e
10	8, 9	cop 4838	. . . 4 class ⟨(+g‘ndx), +e ⟩
11		cmulr 17455	. . . . . 6 class .r
12	2, 11	cfv 6555	. . . . 5 class (.r‘ndx)
13		cxmu 13264	. . . . 5 class ·e
14	12, 13	cop 4838	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4592	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17460	. . . . . 6 class TopSet
17	2, 16	cfv 6555	. . . . 5 class (TopSet‘ndx)
18		cle 11368	. . . . . 6 class ≤
19		cordt 17697	. . . . . 6 class ordTop
20	18, 19	cfv 6555	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4838	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17461	. . . . . 6 class le
23	2, 22	cfv 6555	. . . . 5 class (le‘ndx)
24	23, 18	cop 4838	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17463	. . . . . 6 class dist
26	2, 25	cfv 6555	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1569	. . . . . . . 8 class 𝑥
30	28	cv 1569	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5106	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13262	. . . . . . . 8 class -e𝑥
33	30, 32, 9	co 7440	. . . . . . 7 class (𝑦 +e -e𝑥)
34	30	cxne 13262	. . . . . . . 8 class -e𝑦
35	29, 34, 9	co 7440	. . . . . . 7 class (𝑥 +e -e𝑦)
36	31, 33, 35	cif 4485	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦))
37	27, 28, 5, 5, 36	cmpo 7442	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))
38	26, 37	cop 4838	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩
39	21, 24, 38	ctp 4592	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩}
40	15, 39	cun 4152	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})
41	1, 40	wceq 1570	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +e ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +e -e𝑥), (𝑥 +e -e𝑦)))⟩})

This definition is used by:  xrsle  17802  xrsbas  17804  xrsstr  21721  xrsex  21722  xrsadd  21723  xrsmul  21724  xrstset  21725  xrsds  21743