Definition df-xrs 17555

Description: The extended real number structure. Unlike df-cnfld 21502, 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 21502. 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 17553	. 2 class ℝ*𝑠
2		cnx 17252	. . . . . 6 class ndx
3		cbs 17268	. . . . . 6 class Base
4	2, 3	cfv 6536	. . . . 5 class (Base‘ndx)
5		cxr 11241	. . . . 5 class ℝ*
6	4, 5	cop 4594	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17309	. . . . . 6 class +g
8	2, 7	cfv 6536	. . . . 5 class (+g‘ndx)
9		cxad 13134	. . . . 5 class +𝑒
10	8, 9	cop 4594	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17310	. . . . . 6 class .r
12	2, 11	cfv 6536	. . . . 5 class (.r‘ndx)
13		cxmu 13135	. . . . 5 class ·e
14	12, 13	cop 4594	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4592	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17315	. . . . . 6 class TopSet
17	2, 16	cfv 6536	. . . . 5 class (TopSet‘ndx)
18		cle 11243	. . . . . 6 class ≤
19		cordt 17552	. . . . . 6 class ordTop
20	18, 19	cfv 6536	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4594	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17316	. . . . . 6 class le
23	2, 22	cfv 6536	. . . . 5 class (le‘ndx)
24	23, 18	cop 4594	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17318	. . . . . 6 class dist
26	2, 25	cfv 6536	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1567	. . . . . . . 8 class 𝑥
30	28	cv 1567	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5108	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13133	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7410	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13133	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7410	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4486	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7412	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4594	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4592	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3902	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1568	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17657  xrsbas  17659  xrsstr  21517  xrsex  21518  xrsadd  21519  xrsmul  21520  xrstset  21521  xrsds  21539