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 16771
Description: The extended real number structure. Unlike df-cnfld 20096, 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 20096. 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 16769 . 2 class *𝑠
2 cnx 16476 . . . . . 6 class ndx
3 cbs 16479 . . . . . 6 class Base
42, 3cfv 6328 . . . . 5 class (Base‘ndx)
5 cxr 10667 . . . . 5 class *
64, 5cop 4534 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 16561 . . . . . 6 class +g
82, 7cfv 6328 . . . . 5 class (+g‘ndx)
9 cxad 12497 . . . . 5 class +𝑒
108, 9cop 4534 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 16562 . . . . . 6 class .r
122, 11cfv 6328 . . . . 5 class (.r‘ndx)
13 cxmu 12498 . . . . 5 class ·e
1412, 13cop 4534 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4532 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 16567 . . . . . 6 class TopSet
172, 16cfv 6328 . . . . 5 class (TopSet‘ndx)
18 cle 10669 . . . . . 6 class
19 cordt 16768 . . . . . 6 class ordTop
2018, 19cfv 6328 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4534 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 16568 . . . . . 6 class le
232, 22cfv 6328 . . . . 5 class (le‘ndx)
2423, 18cop 4534 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 16570 . . . . . 6 class dist
262, 25cfv 6328 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1537 . . . . . . . 8 class 𝑥
3028cv 1537 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 5033 . . . . . . 7 wff 𝑥𝑦
3229cxne 12496 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 7139 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 12496 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 7139 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4428 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpo 7141 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4534 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4532 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3882 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1538 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  20109  xrsex  20110  xrsbas  20111  xrsadd  20112  xrsmul  20113  xrstset  20114  xrsle  20115  xrsds  20138
  Copyright terms: Public domain W3C validator