Users' Mathboxes 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