Definition df-xrs 17472

Description: The extended real number structure. Unlike df-cnfld 21272, 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 21272. 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 17470	. 2 class ℝ*𝑠
2		cnx 17170	. . . . . 6 class ndx
3		cbs 17186	. . . . . 6 class Base
4	2, 3	cfv 6514	. . . . 5 class (Base‘ndx)
5		cxr 11214	. . . . 5 class ℝ*
6	4, 5	cop 4598	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17227	. . . . . 6 class +g
8	2, 7	cfv 6514	. . . . 5 class (+g‘ndx)
9		cxad 13077	. . . . 5 class +𝑒
10	8, 9	cop 4598	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17228	. . . . . 6 class .r
12	2, 11	cfv 6514	. . . . 5 class (.r‘ndx)
13		cxmu 13078	. . . . 5 class ·e
14	12, 13	cop 4598	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4596	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17233	. . . . . 6 class TopSet
17	2, 16	cfv 6514	. . . . 5 class (TopSet‘ndx)
18		cle 11216	. . . . . 6 class ≤
19		cordt 17469	. . . . . 6 class ordTop
20	18, 19	cfv 6514	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4598	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17234	. . . . . 6 class le
23	2, 22	cfv 6514	. . . . 5 class (le‘ndx)
24	23, 18	cop 4598	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17236	. . . . . 6 class dist
26	2, 25	cfv 6514	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1539	. . . . . . . 8 class 𝑥
30	28	cv 1539	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5110	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13076	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7390	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13076	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7390	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4491	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7392	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4598	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4596	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3915	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1540	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21300  xrsex  21301  xrsbas  21302  xrsadd  21303  xrsmul  21304  xrstset  21305  xrsle  21306  xrsds  21333