Definition df-xrs 17448

Description: The extended real number structure. Unlike df-cnfld 20945, 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 20945. 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 17446	. 2 class ℝ*𝑠
2		cnx 17126	. . . . . 6 class ndx
3		cbs 17144	. . . . . 6 class Base
4	2, 3	cfv 6544	. . . . 5 class (Base‘ndx)
5		cxr 11247	. . . . 5 class ℝ*
6	4, 5	cop 4635	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17197	. . . . . 6 class +g
8	2, 7	cfv 6544	. . . . 5 class (+g‘ndx)
9		cxad 13090	. . . . 5 class +𝑒
10	8, 9	cop 4635	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17198	. . . . . 6 class .r
12	2, 11	cfv 6544	. . . . 5 class (.r‘ndx)
13		cxmu 13091	. . . . 5 class ·e
14	12, 13	cop 4635	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4633	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17203	. . . . . 6 class TopSet
17	2, 16	cfv 6544	. . . . 5 class (TopSet‘ndx)
18		cle 11249	. . . . . 6 class ≤
19		cordt 17445	. . . . . 6 class ordTop
20	18, 19	cfv 6544	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4635	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17204	. . . . . 6 class le
23	2, 22	cfv 6544	. . . . 5 class (le‘ndx)
24	23, 18	cop 4635	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17206	. . . . . 6 class dist
26	2, 25	cfv 6544	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1541	. . . . . . . 8 class 𝑥
30	28	cv 1541	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5149	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13089	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7409	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13089	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7409	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4529	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7411	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4635	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4633	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3947	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1542	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20959  xrsex  20960  xrsbas  20961  xrsadd  20962  xrsmul  20963  xrstset  20964  xrsle  20965  xrsds  20988