Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rrext Structured version   Visualization version   GIF version

Definition df-rrext 29825
 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 29826 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
StepHypRef Expression
1 crrext 29820 . 2 class ℝExt
2 vr . . . . . . . 8 setvar 𝑟
32cv 1479 . . . . . . 7 class 𝑟
4 czlm 19768 . . . . . . 7 class ℤMod
53, 4cfv 5847 . . . . . 6 class (ℤMod‘𝑟)
6 cnlm 22295 . . . . . 6 class NrmMod
75, 6wcel 1987 . . . . 5 wff (ℤMod‘𝑟) ∈ NrmMod
8 cchr 19769 . . . . . . 7 class chr
93, 8cfv 5847 . . . . . 6 class (chr‘𝑟)
10 cc0 9880 . . . . . 6 class 0
119, 10wceq 1480 . . . . 5 wff (chr‘𝑟) = 0
127, 11wa 384 . . . 4 wff ((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0)
13 ccusp 22011 . . . . . 6 class CUnifSp
143, 13wcel 1987 . . . . 5 wff 𝑟 ∈ CUnifSp
15 cuss 21967 . . . . . . 7 class UnifSt
163, 15cfv 5847 . . . . . 6 class (UnifSt‘𝑟)
17 cds 15871 . . . . . . . . 9 class dist
183, 17cfv 5847 . . . . . . . 8 class (dist‘𝑟)
19 cbs 15781 . . . . . . . . . 10 class Base
203, 19cfv 5847 . . . . . . . . 9 class (Base‘𝑟)
2120, 20cxp 5072 . . . . . . . 8 class ((Base‘𝑟) × (Base‘𝑟))
2218, 21cres 5076 . . . . . . 7 class ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))
23 cmetu 19656 . . . . . . 7 class metUnif
2422, 23cfv 5847 . . . . . 6 class (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2516, 24wceq 1480 . . . . 5 wff (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2614, 25wa 384 . . . 4 wff (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))
2712, 26wa 384 . . 3 wff (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))
28 cnrg 22294 . . . 4 class NrmRing
29 cdr 18668 . . . 4 class DivRing
3028, 29cin 3554 . . 3 class (NrmRing ∩ DivRing)
3127, 2, 30crab 2911 . 2 class {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
321, 31wceq 1480 1 wff ℝExt = {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
 Colors of variables: wff setvar class This definition is referenced by:  isrrext  29826
 Copyright terms: Public domain W3C validator