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 16209
Description: The extended real number structure. Unlike df-cnfld 19795, 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 19795. 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 16207 . 2 class *𝑠
2 cnx 15901 . . . . . 6 class ndx
3 cbs 15904 . . . . . 6 class Base
42, 3cfv 5926 . . . . 5 class (Base‘ndx)
5 cxr 10111 . . . . 5 class *
64, 5cop 4216 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 15988 . . . . . 6 class +g
82, 7cfv 5926 . . . . 5 class (+g‘ndx)
9 cxad 11982 . . . . 5 class +𝑒
108, 9cop 4216 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 15989 . . . . . 6 class .r
122, 11cfv 5926 . . . . 5 class (.r‘ndx)
13 cxmu 11983 . . . . 5 class ·e
1412, 13cop 4216 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4214 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 15994 . . . . . 6 class TopSet
172, 16cfv 5926 . . . . 5 class (TopSet‘ndx)
18 cle 10113 . . . . . 6 class
19 cordt 16206 . . . . . 6 class ordTop
2018, 19cfv 5926 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4216 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 15995 . . . . . 6 class le
232, 22cfv 5926 . . . . 5 class (le‘ndx)
2423, 18cop 4216 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 15997 . . . . . 6 class dist
262, 25cfv 5926 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1522 . . . . . . . 8 class 𝑥
3028cv 1522 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 4685 . . . . . . 7 wff 𝑥𝑦
3229cxne 11981 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 6690 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 11981 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 6690 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4119 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpt2 6692 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4216 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4214 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3605 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1523 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  19808  xrsex  19809  xrsbas  19810  xrsadd  19811  xrsmul  19812  xrstset  19813  xrsle  19814  xrsds  19837
  Copyright terms: Public domain W3C validator