Definition df-xrs 17461

Description: The extended real number structure. Unlike df-cnfld 21351, 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 21351. 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 17459	. 2 class ℝ*𝑠
2		cnx 17158	. . . . . 6 class ndx
3		cbs 17174	. . . . . 6 class Base
4	2, 3	cfv 6488	. . . . 5 class (Base‘ndx)
5		cxr 11174	. . . . 5 class ℝ*
6	4, 5	cop 4563	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17215	. . . . . 6 class +g
8	2, 7	cfv 6488	. . . . 5 class (+g‘ndx)
9		cxad 13056	. . . . 5 class +𝑒
10	8, 9	cop 4563	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17216	. . . . . 6 class .r
12	2, 11	cfv 6488	. . . . 5 class (.r‘ndx)
13		cxmu 13057	. . . . 5 class ·e
14	12, 13	cop 4563	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4561	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17221	. . . . . 6 class TopSet
17	2, 16	cfv 6488	. . . . 5 class (TopSet‘ndx)
18		cle 11176	. . . . . 6 class ≤
19		cordt 17458	. . . . . 6 class ordTop
20	18, 19	cfv 6488	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4563	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17222	. . . . . 6 class le
23	2, 22	cfv 6488	. . . . 5 class (le‘ndx)
24	23, 18	cop 4563	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17224	. . . . . 6 class dist
26	2, 25	cfv 6488	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1547	. . . . . . . 8 class 𝑥
30	28	cv 1547	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5074	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13055	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7359	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13055	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7359	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4456	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7361	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4563	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4561	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3882	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1548	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsle  17563  xrsbas  17565  xrsstr  21366  xrsex  21367  xrsadd  21368  xrsmul  21369  xrstset  21370  xrsds  21388