Definition df-xrs 17222

Description: The extended real number structure. Unlike df-cnfld 20607, 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 20607. 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 17220	. 2 class ℝ*𝑠
2		cnx 16903	. . . . . 6 class ndx
3		cbs 16921	. . . . . 6 class Base
4	2, 3	cfv 6437	. . . . 5 class (Base‘ndx)
5		cxr 11017	. . . . 5 class ℝ*
6	4, 5	cop 4568	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16971	. . . . . 6 class +g
8	2, 7	cfv 6437	. . . . 5 class (+g‘ndx)
9		cxad 12855	. . . . 5 class +𝑒
10	8, 9	cop 4568	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16972	. . . . . 6 class .r
12	2, 11	cfv 6437	. . . . 5 class (.r‘ndx)
13		cxmu 12856	. . . . 5 class ·e
14	12, 13	cop 4568	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4566	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16977	. . . . . 6 class TopSet
17	2, 16	cfv 6437	. . . . 5 class (TopSet‘ndx)
18		cle 11019	. . . . . 6 class ≤
19		cordt 17219	. . . . . 6 class ordTop
20	18, 19	cfv 6437	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4568	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16978	. . . . . 6 class le
23	2, 22	cfv 6437	. . . . 5 class (le‘ndx)
24	23, 18	cop 4568	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16980	. . . . . 6 class dist
26	2, 25	cfv 6437	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1538	. . . . . . . 8 class 𝑥
30	28	cv 1538	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5075	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12854	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7284	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12854	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7284	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4460	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7286	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4568	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4566	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3886	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1539	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20621  xrsex  20622  xrsbas  20623  xrsadd  20624  xrsmul  20625  xrstset  20626  xrsle  20627  xrsds  20650