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 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
StepHypRef Expression
1 cxrs 16607 . 2 class *𝑠
2 cnx 16314 . . . . . 6 class ndx
3 cbs 16317 . . . . . 6 class Base
42, 3cfv 6230 . . . . 5 class (Base‘ndx)
5 cxr 10525 . . . . 5 class *
64, 5cop 4482 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 16399 . . . . . 6 class +g
82, 7cfv 6230 . . . . 5 class (+g‘ndx)
9 cxad 12360 . . . . 5 class +𝑒
108, 9cop 4482 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 16400 . . . . . 6 class .r
122, 11cfv 6230 . . . . 5 class (.r‘ndx)
13 cxmu 12361 . . . . 5 class ·e
1412, 13cop 4482 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4480 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 16405 . . . . . 6 class TopSet
172, 16cfv 6230 . . . . 5 class (TopSet‘ndx)
18 cle 10527 . . . . . 6 class
19 cordt 16606 . . . . . 6 class ordTop
2018, 19cfv 6230 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4482 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 16406 . . . . . 6 class le
232, 22cfv 6230 . . . . 5 class (le‘ndx)
2423, 18cop 4482 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 16408 . . . . . 6 class dist
262, 25cfv 6230 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1521 . . . . . . . 8 class 𝑥
3028cv 1521 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 4966 . . . . . . 7 wff 𝑥𝑦
3229cxne 12359 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 7021 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 12359 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 7021 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4385 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpo 7023 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4482 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4480 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3861 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1522 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  20246  xrsex  20247  xrsbas  20248  xrsadd  20249  xrsmul  20250  xrstset  20251  xrsle  20252  xrsds  20275
  Copyright terms: Public domain W3C validator