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