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 16765
Description: The extended real number structure. Unlike df-cnfld 20476, 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 20476. 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 16763 . 2 class *𝑠
2 cnx 16470 . . . . . 6 class ndx
3 cbs 16473 . . . . . 6 class Base
42, 3cfv 6349 . . . . 5 class (Base‘ndx)
5 cxr 10663 . . . . 5 class *
64, 5cop 4565 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 16555 . . . . . 6 class +g
82, 7cfv 6349 . . . . 5 class (+g‘ndx)
9 cxad 12495 . . . . 5 class +𝑒
108, 9cop 4565 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 16556 . . . . . 6 class .r
122, 11cfv 6349 . . . . 5 class (.r‘ndx)
13 cxmu 12496 . . . . 5 class ·e
1412, 13cop 4565 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4563 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 16561 . . . . . 6 class TopSet
172, 16cfv 6349 . . . . 5 class (TopSet‘ndx)
18 cle 10665 . . . . . 6 class
19 cordt 16762 . . . . . 6 class ordTop
2018, 19cfv 6349 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4565 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 16562 . . . . . 6 class le
232, 22cfv 6349 . . . . 5 class (le‘ndx)
2423, 18cop 4565 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 16564 . . . . . 6 class dist
262, 25cfv 6349 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1527 . . . . . . . 8 class 𝑥
3028cv 1527 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 5058 . . . . . . 7 wff 𝑥𝑦
3229cxne 12494 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 7145 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 12494 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 7145 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4465 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpo 7147 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4565 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4563 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3933 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1528 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  20489  xrsex  20490  xrsbas  20491  xrsadd  20492  xrsmul  20493  xrstset  20494  xrsle  20495  xrsds  20518
  Copyright terms: Public domain W3C validator