Definition df-xrs 17514

Description: The extended real number structure. Unlike df-cnfld 21314, 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 21314. 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 17512	. 2 class ℝ*𝑠
2		cnx 17210	. . . . . 6 class ndx
3		cbs 17226	. . . . . 6 class Base
4	2, 3	cfv 6530	. . . . 5 class (Base‘ndx)
5		cxr 11266	. . . . 5 class ℝ*
6	4, 5	cop 4607	. . . 4 class ⟨(Base‘ndx), ℝ*⟩
7		cplusg 17269	. . . . . 6 class +g
8	2, 7	cfv 6530	. . . . 5 class (+g‘ndx)
9		cxad 13124	. . . . 5 class +𝑒
10	8, 9	cop 4607	. . . 4 class ⟨(+g‘ndx), +𝑒 ⟩
11		cmulr 17270	. . . . . 6 class .r
12	2, 11	cfv 6530	. . . . 5 class (.r‘ndx)
13		cxmu 13125	. . . . 5 class ·e
14	12, 13	cop 4607	. . . 4 class ⟨(.r‘ndx), ·e ⟩
15	6, 10, 14	ctp 4605	. . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16		cts 17275	. . . . . 6 class TopSet
17	2, 16	cfv 6530	. . . . 5 class (TopSet‘ndx)
18		cle 11268	. . . . . 6 class ≤
19		cordt 17511	. . . . . 6 class ordTop
20	18, 19	cfv 6530	. . . . 5 class (ordTop‘ ≤ )
21	17, 20	cop 4607	. . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22		cple 17276	. . . . . 6 class le
23	2, 22	cfv 6530	. . . . 5 class (le‘ndx)
24	23, 18	cop 4607	. . . 4 class ⟨(le‘ndx), ≤ ⟩
25		cds 17278	. . . . . 6 class dist
26	2, 25	cfv 6530	. . . . 5 class (dist‘ndx)
27		vx	. . . . . 6 setvar 𝑥
28		vy	. . . . . 6 setvar 𝑦
29	27	cv 1539	. . . . . . . 8 class 𝑥
30	28	cv 1539	. . . . . . . 8 class 𝑦
31	29, 30, 18	wbr 5119	. . . . . . 7 wff 𝑥 ≤ 𝑦
32	29	cxne 13123	. . . . . . . 8 class -𝑒𝑥
33	30, 32, 9	co 7403	. . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
34	30	cxne 13123	. . . . . . . 8 class -𝑒𝑦
35	29, 34, 9	co 7403	. . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
36	31, 33, 35	cif 4500	. . . . . 6 class if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
37	27, 28, 5, 5, 36	cmpo 7405	. . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
38	26, 37	cop 4607	. . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
39	21, 24, 38	ctp 4605	. . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
40	15, 39	cun 3924	. 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
41	1, 40	wceq 1540	1 wff ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})

This definition is referenced by:  xrsstr  21342  xrsex  21343  xrsbas  21344  xrsadd  21345  xrsmul  21346  xrstset  21347  xrsle  21348  xrsds  21375