Definition df-rrext 30043

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 30044 for a better readable version. (Contributed by Thierry Arnoux, 2-May-2018.)

Assertion

Ref	Expression
df-rrext	|- ℝExt = { r e. (NrmRing i^i DivRing ) | ( ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) }

Detailed syntax breakdown of Definition df-rrext

Step	Hyp	Ref	Expression
1		crrext 30038	. 2 class ℝExt
2		vr	. . . . . . . 8 setvar r
3	2	cv 1482	. . . . . . 7 class r
4		czlm 19849	. . . . . . 7 class ZMod
5	3, 4	cfv 5888	. . . . . 6 class ( ZMod ` r )
6		cnlm 22385	. . . . . 6 class NrmMod
7	5, 6	wcel 1990	. . . . 5 wff ( ZMod ` r ) e. NrmMod
8		cchr 19850	. . . . . . 7 class chr
9	3, 8	cfv 5888	. . . . . 6 class (chr ` r )
10		cc0 9936	. . . . . 6 class 0
11	9, 10	wceq 1483	. . . . 5 wff (chr ` r ) = 0
12	7, 11	wa 384	. . . 4 wff ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 )
13		ccusp 22101	. . . . . 6 class CUnifSp
14	3, 13	wcel 1990	. . . . 5 wff r e. CUnifSp
15		cuss 22057	. . . . . . 7 class UnifSt
16	3, 15	cfv 5888	. . . . . 6 class (UnifSt ` r )
17		cds 15950	. . . . . . . . 9 class dist
18	3, 17	cfv 5888	. . . . . . . 8 class ( dist ` r )
19		cbs 15857	. . . . . . . . . 10 class Base
20	3, 19	cfv 5888	. . . . . . . . 9 class ( Base ` r )
21	20, 20	cxp 5112	. . . . . . . 8 class ( ( Base ` r ) X. ( Base ` r ) )
22	18, 21	cres 5116	. . . . . . 7 class ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) )
23		cmetu 19737	. . . . . . 7 class metUnif
24	22, 23	cfv 5888	. . . . . 6 class (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) )
25	16, 24	wceq 1483	. . . . 5 wff (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) )
26	14, 25	wa 384	. . . 4 wff ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) )
27	12, 26	wa 384	. . 3 wff ( ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) )
28		cnrg 22384	. . . 4 class NrmRing
29		cdr 18747	. . . 4 class DivRing
30	28, 29	cin 3573	. . 3 class (NrmRing i^i DivRing )
31	27, 2, 30	crab 2916	. 2 class { r e. (NrmRing i^i DivRing ) | ( ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) }
32	1, 31	wceq 1483	1 wff ℝExt = { r e. (NrmRing i^i DivRing ) | ( ( ( ZMod ` r ) e. NrmMod /\ (chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ (UnifSt ` r ) = (metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) }

This definition is referenced by:  isrrext  30044