Definition df-xrs 17445

Description: The extended real number structure. Unlike df-cnfld 20938, 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 20938. 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 17443	. 2 class ℝ*𝑠
2		cnx 17123	. . . . . 6 class ndx
3		cbs 17141	. . . . . 6 class Base
4	2, 3	cfv 6541	. . . . 5 class (Base‘ndx)
5		cxr 11244	. . . . 5 class ℝ*
6	4, 5	cop 4634	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17194	. . . . . 6 class +g
8	2, 7	cfv 6541	. . . . 5 class (+g‘ndx)
9		cxad 13087	. . . . 5 class +𝑒
10	8, 9	cop 4634	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17195	. . . . . 6 class .r
12	2, 11	cfv 6541	. . . . 5 class (.r‘ndx)
13		cxmu 13088	. . . . 5 class ·e
14	12, 13	cop 4634	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4632	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17200	. . . . . 6 class TopSet
17	2, 16	cfv 6541	. . . . 5 class (TopSet‘ndx)
18		cle 11246	. . . . . 6 class ≤
19		cordt 17442	. . . . . 6 class ordTop
20	18, 19	cfv 6541	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4634	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17201	. . . . . 6 class le
23	2, 22	cfv 6541	. . . . 5 class (le‘ndx)
24	23, 18	cop 4634	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17203	. . . . . 6 class dist
26	2, 25	cfv 6541	. . . . 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 5148	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13086	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7406	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13086	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7406	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4528	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7408	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4634	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4632	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3946	. 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  20952  xrsex  20953  xrsbas  20954  xrsadd  20955  xrsmul  20956  xrstset  20957  xrsle  20958  xrsds  20981