This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-xrs

Description: The extended real number structure. Unlike df-cnfld , 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 . 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 +oo is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +oo an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with CCfld when restricted to RR . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion df-xrs ⊢ ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxrs class ℝ 𝑠 *
1 cbs class Base
2 cnx class ndx
3 2 1 cfv class Base ndx
4 cxr class ℝ *
5 3 4 cop class Base ndx ℝ *
6 cplusg class + 𝑔
7 2 6 cfv class + ndx
8 cxad class + 𝑒
9 7 8 cop class + ndx + 𝑒
10 cmulr class ⋅ 𝑟
11 2 10 cfv class ⋅ ndx
12 cxmu class ⋅ 𝑒
13 11 12 cop class ⋅ ndx ⋅ 𝑒
14 5 9 13 ctp class Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒
15 cts class TopSet
16 2 15 cfv class TopSet ⁡ ndx
17 cordt class ordTop
18 cle class ≤
19 18 17 cfv class ordTop ⁡ ≤
20 16 19 cop class TopSet ⁡ ndx ordTop ⁡ ≤
21 cple class le
22 2 21 cfv class ≤ ndx
23 22 18 cop class ≤ ndx ≤
24 cds class dist
25 2 24 cfv class dist ⁡ ndx
26 vx setvar x
27 vy setvar y
28 26 cv setvar x
29 27 cv setvar y
30 28 29 18 wbr wff x ≤ y
31 28 cxne class − x
32 29 31 8 co class y + 𝑒 − x
33 29 cxne class − y
34 28 33 8 co class x + 𝑒 − y
35 30 32 34 cif class if x ≤ y y + 𝑒 − x x + 𝑒 − y
36 26 27 4 4 35 cmpo class x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
37 25 36 cop class dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
38 20 23 37 ctp class TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
39 14 38 cun class Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
40 0 39 wceq wff ℝ 𝑠 * = Base ndx ℝ * + ndx + 𝑒 ⋅ ndx ⋅ 𝑒 ∪ TopSet ⁡ ndx ordTop ⁡ ≤ ≤ ndx ≤ dist ⁡ ndx x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y