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	|- RRExt = { 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

Step	Hyp	Ref	Expression
0		crrext	|- RRExt
1		vr	|- r
2		cnrg	|- NrmRing
3		cdr	|- DivRing
4	2 3	cin	|- ( NrmRing i^i DivRing )
5		czlm	|- ZMod
6	1	cv	|- r
7	6 5	cfv	|- ( ZMod ` r )
8		cnlm	|- NrmMod
9	7 8	wcel	|- ( ZMod ` r ) e. NrmMod
10		cchr	|- chr
11	6 10	cfv	|- ( chr ` r )
12		cc0	|- 0
13	11 12	wceq	|- ( chr ` r ) = 0
14	9 13	wa	|- ( ( ZMod ` r ) e. NrmMod /\ ( chr ` r ) = 0 )
15		ccusp	|- CUnifSp
16	6 15	wcel	|- r e. CUnifSp
17		cuss	|- UnifSt
18	6 17	cfv	|- ( UnifSt ` r )
19		cmetu	|- metUnif
20		cds	|- dist
21	6 20	cfv	|- ( dist ` r )
22		cbs	|- Base
23	6 22	cfv	|- ( Base ` r )
24	23 23	cxp	|- ( ( Base ` r ) X. ( Base ` r ) )
25	21 24	cres	|- ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) )
26	25 19	cfv	|- ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) )
27	18 26	wceq	|- ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) )
28	16 27	wa	|- ( r e. CUnifSp /\ ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) )
29	14 28	wa	|- ( ( ( ZMod ` r ) e. NrmMod /\ ( chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) )
30	29 1 4	crab	|- { 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 ) ) ) ) ) ) }
31	0 30	wceq	|- RRExt = { 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 ) ) ) ) ) ) }