Definition df-rrext 31350

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

Assertion

Ref	Expression
df-rrext	⊢ ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}

Detailed syntax breakdown of Definition df-rrext

Step	Hyp	Ref	Expression
1		crrext 31345	. 2 class ℝExt
2		vr	. . . . . . . 8 setvar 𝑟
3	2	cv 1537	. . . . . . 7 class 𝑟
4		czlm 20194	. . . . . . 7 class ℤMod
5	3, 4	cfv 6324	. . . . . 6 class (ℤMod‘𝑟)
6		cnlm 23187	. . . . . 6 class NrmMod
7	5, 6	wcel 2111	. . . . 5 wff (ℤMod‘𝑟) ∈ NrmMod
8		cchr 20195	. . . . . . 7 class chr
9	3, 8	cfv 6324	. . . . . 6 class (chr‘𝑟)
10		cc0 10526	. . . . . 6 class 0
11	9, 10	wceq 1538	. . . . 5 wff (chr‘𝑟) = 0
12	7, 11	wa 399	. . . 4 wff ((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0)
13		ccusp 22903	. . . . . 6 class CUnifSp
14	3, 13	wcel 2111	. . . . 5 wff 𝑟 ∈ CUnifSp
15		cuss 22859	. . . . . . 7 class UnifSt
16	3, 15	cfv 6324	. . . . . 6 class (UnifSt‘𝑟)
17		cds 16566	. . . . . . . . 9 class dist
18	3, 17	cfv 6324	. . . . . . . 8 class (dist‘𝑟)
19		cbs 16475	. . . . . . . . . 10 class Base
20	3, 19	cfv 6324	. . . . . . . . 9 class (Base‘𝑟)
21	20, 20	cxp 5517	. . . . . . . 8 class ((Base‘𝑟) × (Base‘𝑟))
22	18, 21	cres 5521	. . . . . . 7 class ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))
23		cmetu 20082	. . . . . . 7 class metUnif
24	22, 23	cfv 6324	. . . . . 6 class (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
25	16, 24	wceq 1538	. . . . 5 wff (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
26	14, 25	wa 399	. . . 4 wff (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))
27	12, 26	wa 399	. . 3 wff (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))
28		cnrg 23186	. . . 4 class NrmRing
29		cdr 19495	. . . 4 class DivRing
30	28, 29	cin 3880	. . 3 class (NrmRing ∩ DivRing)
31	27, 2, 30	crab 3110	. 2 class {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
32	1, 31	wceq 1538	1 wff ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}

This definition is referenced by:  isrrext  31351