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 17547
Description: The extended real number structure. Unlike df-cnfld 21365, 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 21365. 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 17545 . 2 class *𝑠
2 cnx 17230 . . . . . 6 class ndx
3 cbs 17247 . . . . . 6 class Base
42, 3cfv 6561 . . . . 5 class (Base‘ndx)
5 cxr 11294 . . . . 5 class *
64, 5cop 4632 . . . 4 class ⟨(Base‘ndx), ℝ*
7 cplusg 17297 . . . . . 6 class +g
82, 7cfv 6561 . . . . 5 class (+g‘ndx)
9 cxad 13152 . . . . 5 class +𝑒
108, 9cop 4632 . . . 4 class ⟨(+g‘ndx), +𝑒
11 cmulr 17298 . . . . . 6 class .r
122, 11cfv 6561 . . . . 5 class (.r‘ndx)
13 cxmu 13153 . . . . 5 class ·e
1412, 13cop 4632 . . . 4 class ⟨(.r‘ndx), ·e
156, 10, 14ctp 4630 . . 3 class {⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩}
16 cts 17303 . . . . . 6 class TopSet
172, 16cfv 6561 . . . . 5 class (TopSet‘ndx)
18 cle 11296 . . . . . 6 class
19 cordt 17544 . . . . . 6 class ordTop
2018, 19cfv 6561 . . . . 5 class (ordTop‘ ≤ )
2117, 20cop 4632 . . . 4 class ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩
22 cple 17304 . . . . . 6 class le
232, 22cfv 6561 . . . . 5 class (le‘ndx)
2423, 18cop 4632 . . . 4 class ⟨(le‘ndx), ≤ ⟩
25 cds 17306 . . . . . 6 class dist
262, 25cfv 6561 . . . . 5 class (dist‘ndx)
27 vx . . . . . 6 setvar 𝑥
28 vy . . . . . 6 setvar 𝑦
2927cv 1539 . . . . . . . 8 class 𝑥
3028cv 1539 . . . . . . . 8 class 𝑦
3129, 30, 18wbr 5143 . . . . . . 7 wff 𝑥𝑦
3229cxne 13151 . . . . . . . 8 class -𝑒𝑥
3330, 32, 9co 7431 . . . . . . 7 class (𝑦 +𝑒 -𝑒𝑥)
3430cxne 13151 . . . . . . . 8 class -𝑒𝑦
3529, 34, 9co 7431 . . . . . . 7 class (𝑥 +𝑒 -𝑒𝑦)
3631, 33, 35cif 4525 . . . . . 6 class if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦))
3727, 28, 5, 5, 36cmpo 7433 . . . . 5 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))
3826, 37cop 4632 . . . 4 class ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩
3921, 24, 38ctp 4630 . . 3 class {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩}
4015, 39cun 3949 . 2 class ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
411, 40wceq 1540 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  21394  xrsex  21395  xrsbas  21396  xrsadd  21397  xrsmul  21398  xrstset  21399  xrsle  21400  xrsds  21427
  Copyright terms: Public domain W3C validator