MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xrs Structured version   Visualization version   GIF version

Definition df-xrs 15985
Description: The extended real number structure. Unlike df-cnfld 19568, 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 19568. 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
StepHypRef Expression
1 cxrs 15983 . 2 class *𝑠
2 cnx 15692 . . . . . 6 class ndx
3 cbs 15695 . . . . . 6 class Base
42, 3cfv 5804 . . . . 5 class (Base‘ndx)
5 cxr 9952 . . . . 5 class *
64, 5cop 4131 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 15768 . . . . . 6 class +g
82, 7cfv 5804 . . . . 5 class (+g‘ndx)
9 cxad 11820 . . . . 5 class +𝑒
108, 9cop 4131 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 15769 . . . . . 6 class .r
122, 11cfv 5804 . . . . 5 class (.r‘ndx)
13 cxmu 11821 . . . . 5 class ·e
1412, 13cop 4131 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4129 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 15774 . . . . . 6 class TopSet
172, 16cfv 5804 . . . . 5 class (TopSet‘ndx)
18 cle 9954 . . . . . 6 class
19 cordt 15982 . . . . . 6 class ordTop
2018, 19cfv 5804 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4131 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 15775 . . . . . 6 class le
232, 22cfv 5804 . . . . 5 class (le‘ndx)
2423, 18cop 4131 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 15777 . . . . . 6 class dist
262, 25cfv 5804 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1474 . . . . . . . 8 class 𝑥
3028cv 1474 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 4583 . . . . . . 7 wff 𝑥𝑦
3229cxne 11819 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 6549 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 11819 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 6549 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4036 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpt2 6551 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4131 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4129 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3538 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1475 1 wff *𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  xrsstr  19579  xrsex  19580  xrsbas  19581  xrsadd  19582  xrsmul  19583  xrstset  19584  xrsle  19585  xrsds  19608
  Copyright terms: Public domain W3C validator