Definition df-xrs 17408

Description: The extended real number structure. Unlike df-cnfld 21294, 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 21294. 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 17406	. 2 class ℝ*𝑠
2		cnx 17106	. . . . . 6 class ndx
3		cbs 17122	. . . . . 6 class Base
4	2, 3	cfv 6486	. . . . 5 class (Base‘ndx)
5		cxr 11152	. . . . 5 class ℝ*
6	4, 5	cop 4581	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17163	. . . . . 6 class +g
8	2, 7	cfv 6486	. . . . 5 class (+g‘ndx)
9		cxad 13011	. . . . 5 class +𝑒
10	8, 9	cop 4581	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17164	. . . . . 6 class .r
12	2, 11	cfv 6486	. . . . 5 class (.r‘ndx)
13		cxmu 13012	. . . . 5 class ·e
14	12, 13	cop 4581	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4579	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17169	. . . . . 6 class TopSet
17	2, 16	cfv 6486	. . . . 5 class (TopSet‘ndx)
18		cle 11154	. . . . . 6 class ≤
19		cordt 17405	. . . . . 6 class ordTop
20	18, 19	cfv 6486	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4581	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17170	. . . . . 6 class le
23	2, 22	cfv 6486	. . . . 5 class (le‘ndx)
24	23, 18	cop 4581	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17172	. . . . . 6 class dist
26	2, 25	cfv 6486	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1540	. . . . . . . 8 class 𝑥
30	28	cv 1540	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5093	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13010	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7352	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13010	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7352	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4474	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7354	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4581	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4579	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3896	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1541	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17510  xrsbas  17512  xrsstr  21322  xrsex  21323  xrsadd  21324  xrsmul  21325  xrstset  21326  xrsds  21348