Metamath Proof Explorer

Definition df-rrext

Description: Define the class of extensions of RR . This is a shorthand for listing the necessary conditions for a structure to admit a canonical embedding of RR into it. Interestingly, this is not coming from a mathematical reference, but was from the necessary conditions to build the embedding at each step ( ZZ , QQ and RR ). It would be interesting see if this is formally treated in the literature. See isrrext for a better readable version. (Contributed by Thierry Arnoux, 2-May-2018)

Ref Expression
Assertion df-rrext ⊢ ℝExt = r ∈ NrmRing ∩ DivRing | ℤMod ⁡ r ∈ NrmMod ∧ chr ⁡ r = 0 ∧ r ∈ CUnifSp ∧ UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrext class ℝExt
1 vr setvar r
2 cnrg class NrmRing
3 cdr class DivRing
4 2 3 cin class NrmRing ∩ DivRing
5 czlm class ℤMod
6 1 cv setvar r
7 6 5 cfv class ℤMod ⁡ r
8 cnlm class NrmMod
9 7 8 wcel wff ℤMod ⁡ r ∈ NrmMod
10 cchr class chr
11 6 10 cfv class chr ⁡ r
12 cc0 class 0
13 11 12 wceq wff chr ⁡ r = 0
14 9 13 wa wff ℤMod ⁡ r ∈ NrmMod ∧ chr ⁡ r = 0
15 ccusp class CUnifSp
16 6 15 wcel wff r ∈ CUnifSp
17 cuss class UnifSt
18 6 17 cfv class UnifSt ⁡ r
19 cmetu class metUnif
20 cds class dist
21 6 20 cfv class dist ⁡ r
22 cbs class Base
23 6 22 cfv class Base r
24 23 23 cxp class Base r × Base r
25 21 24 cres class dist ⁡ r ↾ Base r × Base r
26 25 19 cfv class metUnif ⁡ dist ⁡ r ↾ Base r × Base r
27 18 26 wceq wff UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r
28 16 27 wa wff r ∈ CUnifSp ∧ UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r
29 14 28 wa wff ℤMod ⁡ r ∈ NrmMod ∧ chr ⁡ r = 0 ∧ r ∈ CUnifSp ∧ UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r
30 29 1 4 crab class r ∈ NrmRing ∩ DivRing | ℤMod ⁡ r ∈ NrmMod ∧ chr ⁡ r = 0 ∧ r ∈ CUnifSp ∧ UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r
31 0 30 wceq wff ℝExt = r ∈ NrmRing ∩ DivRing | ℤMod ⁡ r ∈ NrmMod ∧ chr ⁡ r = 0 ∧ r ∈ CUnifSp ∧ UnifSt ⁡ r = metUnif ⁡ dist ⁡ r ↾ Base r × Base r