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 29371
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 29372 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 29366 . 2 class ℝExt
2 vr . . . . . . . 8 setvar 𝑟
32cv 1474 . . . . . . 7 class 𝑟
4 czlm 19668 . . . . . . 7 class ℤMod
53, 4cfv 5804 . . . . . 6 class (ℤMod‘𝑟)
6 cnlm 22195 . . . . . 6 class NrmMod
75, 6wcel 1977 . . . . 5 wff (ℤMod‘𝑟) ∈ NrmMod
8 cchr 19669 . . . . . . 7 class chr
93, 8cfv 5804 . . . . . 6 class (chr‘𝑟)
10 cc0 9815 . . . . . 6 class 0
119, 10wceq 1475 . . . . 5 wff (chr‘𝑟) = 0
127, 11wa 383 . . . 4 wff ((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0)
13 ccusp 21911 . . . . . 6 class CUnifSp
143, 13wcel 1977 . . . . 5 wff 𝑟 ∈ CUnifSp
15 cuss 21867 . . . . . . 7 class UnifSt
163, 15cfv 5804 . . . . . 6 class (UnifSt‘𝑟)
17 cds 15777 . . . . . . . . 9 class dist
183, 17cfv 5804 . . . . . . . 8 class (dist‘𝑟)
19 cbs 15695 . . . . . . . . . 10 class Base
203, 19cfv 5804 . . . . . . . . 9 class (Base‘𝑟)
2120, 20cxp 5036 . . . . . . . 8 class ((Base‘𝑟) × (Base‘𝑟))
2218, 21cres 5040 . . . . . . 7 class ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))
23 cmetu 19558 . . . . . . 7 class metUnif
2422, 23cfv 5804 . . . . . 6 class (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2516, 24wceq 1475 . . . . 5 wff (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2614, 25wa 383 . . . 4 wff (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))
2712, 26wa 383 . . 3 wff (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))
28 cnrg 22194 . . . 4 class NrmRing
29 cdr 18570 . . . 4 class DivRing
3028, 29cin 3539 . . 3 class (NrmRing ∩ DivRing)
3127, 2, 30crab 2900 . 2 class {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
321, 31wceq 1475 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  29372
  Copyright terms: Public domain W3C validator