Definition df-xrs 17548

Description: The extended real number structure. Unlike df-cnfld 21382, 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 21382. 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 17546	. 2 class ℝ*𝑠
2		cnx 17226	. . . . . 6 class ndx
3		cbs 17244	. . . . . 6 class Base
4	2, 3	cfv 6562	. . . . 5 class (Base‘ndx)
5		cxr 11291	. . . . 5 class ℝ*
6	4, 5	cop 4636	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17297	. . . . . 6 class +g
8	2, 7	cfv 6562	. . . . 5 class (+g‘ndx)
9		cxad 13149	. . . . 5 class +𝑒
10	8, 9	cop 4636	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17298	. . . . . 6 class .r
12	2, 11	cfv 6562	. . . . 5 class (.r‘ndx)
13		cxmu 13150	. . . . 5 class ·e
14	12, 13	cop 4636	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4634	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17303	. . . . . 6 class TopSet
17	2, 16	cfv 6562	. . . . 5 class (TopSet‘ndx)
18		cle 11293	. . . . . 6 class ≤
19		cordt 17545	. . . . . 6 class ordTop
20	18, 19	cfv 6562	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4636	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17304	. . . . . 6 class le
23	2, 22	cfv 6562	. . . . 5 class (le‘ndx)
24	23, 18	cop 4636	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17306	. . . . . 6 class dist
26	2, 25	cfv 6562	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1535	. . . . . . . 8 class 𝑥
30	28	cv 1535	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5147	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13148	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7430	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13148	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7430	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4530	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7432	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4636	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4634	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3960	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1536	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21411  xrsex  21412  xrsbas  21413  xrsadd  21414  xrsmul  21415  xrstset  21416  xrsle  21417  xrsds  21444