Definition df-xrs 16609

Description: The extended real number structure. Unlike df-cnfld 20233, 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 20233. 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 16607	. 2 class ℝ*𝑠
2		cnx 16314	. . . . . 6 class ndx
3		cbs 16317	. . . . . 6 class Base
4	2, 3	cfv 6230	. . . . 5 class (Base‘ndx)
5		cxr 10525	. . . . 5 class ℝ*
6	4, 5	cop 4482	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 16399	. . . . . 6 class +g
8	2, 7	cfv 6230	. . . . 5 class (+g‘ndx)
9		cxad 12360	. . . . 5 class +𝑒
10	8, 9	cop 4482	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 16400	. . . . . 6 class .r
12	2, 11	cfv 6230	. . . . 5 class (.r‘ndx)
13		cxmu 12361	. . . . 5 class ·e
14	12, 13	cop 4482	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4480	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 16405	. . . . . 6 class TopSet
17	2, 16	cfv 6230	. . . . 5 class (TopSet‘ndx)
18		cle 10527	. . . . . 6 class ≤
19		cordt 16606	. . . . . 6 class ordTop
20	18, 19	cfv 6230	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4482	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 16406	. . . . . 6 class le
23	2, 22	cfv 6230	. . . . 5 class (le‘ndx)
24	23, 18	cop 4482	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 16408	. . . . . 6 class dist
26	2, 25	cfv 6230	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1521	. . . . . . . 8 class 𝑥
30	28	cv 1521	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 4966	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 12359	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7021	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 12359	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7021	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4385	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7023	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4482	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4480	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3861	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1522	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  20246  xrsex  20247  xrsbas  20248  xrsadd  20249  xrsmul  20250  xrstset  20251  xrsle  20252  xrsds  20275