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 31314
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 31315 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 31309 . 2 class ℝExt
2 vr . . . . . . . 8 setvar 𝑟
32cv 1537 . . . . . . 7 class 𝑟
4 czlm 20192 . . . . . . 7 class ℤMod
53, 4cfv 6334 . . . . . 6 class (ℤMod‘𝑟)
6 cnlm 23185 . . . . . 6 class NrmMod
75, 6wcel 2114 . . . . 5 wff (ℤMod‘𝑟) ∈ NrmMod
8 cchr 20193 . . . . . . 7 class chr
93, 8cfv 6334 . . . . . 6 class (chr‘𝑟)
10 cc0 10526 . . . . . 6 class 0
119, 10wceq 1538 . . . . 5 wff (chr‘𝑟) = 0
127, 11wa 399 . . . 4 wff ((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0)
13 ccusp 22901 . . . . . 6 class CUnifSp
143, 13wcel 2114 . . . . 5 wff 𝑟 ∈ CUnifSp
15 cuss 22857 . . . . . . 7 class UnifSt
163, 15cfv 6334 . . . . . 6 class (UnifSt‘𝑟)
17 cds 16565 . . . . . . . . 9 class dist
183, 17cfv 6334 . . . . . . . 8 class (dist‘𝑟)
19 cbs 16474 . . . . . . . . . 10 class Base
203, 19cfv 6334 . . . . . . . . 9 class (Base‘𝑟)
2120, 20cxp 5530 . . . . . . . 8 class ((Base‘𝑟) × (Base‘𝑟))
2218, 21cres 5534 . . . . . . 7 class ((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))
23 cmetu 20080 . . . . . . 7 class metUnif
2422, 23cfv 6334 . . . . . 6 class (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2516, 24wceq 1538 . . . . 5 wff (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))
2614, 25wa 399 . . . 4 wff (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟)))))
2712, 26wa 399 . . 3 wff (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))
28 cnrg 23184 . . . 4 class NrmRing
29 cdr 19493 . . . 4 class DivRing
3028, 29cin 3907 . . 3 class (NrmRing ∩ DivRing)
3127, 2, 30crab 3134 . 2 class {𝑟 ∈ (NrmRing ∩ DivRing) ∣ (((ℤMod‘𝑟) ∈ NrmMod ∧ (chr‘𝑟) = 0) ∧ (𝑟 ∈ CUnifSp ∧ (UnifSt‘𝑟) = (metUnif‘((dist‘𝑟) ↾ ((Base‘𝑟) × (Base‘𝑟))))))}
321, 31wceq 1538 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  31315
  Copyright terms: Public domain W3C validator