Definition df-xrs 17635

Description: The extended real number structure. Unlike df-cnfld 21640, 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 21640. 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 17633	. 2 class ℝ*𝑠
2		cnx 17332	. . . . . 6 class ndx
3		cbs 17348	. . . . . 6 class Base
4	2, 3	cfv 6527	. . . . 5 class (Base‘ndx)
5		cxr 11313	. . . . 5 class ℝ*
6	4, 5	cop 4589	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17389	. . . . . 6 class +g
8	2, 7	cfv 6527	. . . . 5 class (+g‘ndx)
9		cxad 13208	. . . . 5 class +𝑒
10	8, 9	cop 4589	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17390	. . . . . 6 class .r
12	2, 11	cfv 6527	. . . . 5 class (.r‘ndx)
13		cxmu 13209	. . . . 5 class ·e
14	12, 13	cop 4589	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4587	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17395	. . . . . 6 class TopSet
17	2, 16	cfv 6527	. . . . 5 class (TopSet‘ndx)
18		cle 11315	. . . . . 6 class ≤
19		cordt 17632	. . . . . 6 class ordTop
20	18, 19	cfv 6527	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4589	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17396	. . . . . 6 class le
23	2, 22	cfv 6527	. . . . 5 class (le‘ndx)
24	23, 18	cop 4589	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17398	. . . . . 6 class dist
26	2, 25	cfv 6527	. . . . 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 5102	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13207	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7408	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13207	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7408	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4481	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7410	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4589	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4587	. . 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 1570	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is used by:  xrsle  17737  xrsbas  17739  xrsstr  21655  xrsex  21656  xrsadd  21657  xrsmul  21658  xrstset  21659  xrsds  21677