Definition df-xrs 16961

Description: The extended real number structure. Unlike df-cnfld 20318, 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 20318. 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 16959	. 2 class ℝ*𝑠
2		cnx 16663	. . . . . 6 class ndx
3		cbs 16666	. . . . . 6 class Base
4	2, 3	cfv 6358	. . . . 5 class (Base‘ndx)
5		cxr 10831	. . . . 5 class ℝ*
6	4, 5	cop 4533	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16749	. . . . . 6 class +g
8	2, 7	cfv 6358	. . . . 5 class (+g‘ndx)
9		cxad 12667	. . . . 5 class +𝑒
10	8, 9	cop 4533	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16750	. . . . . 6 class .r
12	2, 11	cfv 6358	. . . . 5 class (.r‘ndx)
13		cxmu 12668	. . . . 5 class ·e
14	12, 13	cop 4533	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4531	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16755	. . . . . 6 class TopSet
17	2, 16	cfv 6358	. . . . 5 class (TopSet‘ndx)
18		cle 10833	. . . . . 6 class ≤
19		cordt 16958	. . . . . 6 class ordTop
20	18, 19	cfv 6358	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4533	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16756	. . . . . 6 class le
23	2, 22	cfv 6358	. . . . 5 class (le‘ndx)
24	23, 18	cop 4533	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16758	. . . . . 6 class dist
26	2, 25	cfv 6358	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1542	. . . . . . . 8 class 𝑥
30	28	cv 1542	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5039	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12666	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7191	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12666	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7191	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4425	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7193	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4533	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4531	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3851	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1543	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20331  xrsex  20332  xrsbas  20333  xrsadd  20334  xrsmul  20335  xrstset  20336  xrsle  20337  xrsds  20360