Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrextust Structured version   Visualization version   GIF version

Theorem rrextust 31357
Description: The uniformity of an extension of is the uniformity generated by its distance. (Contributed by Thierry Arnoux, 2-May-2018.)
Hypotheses
Ref Expression
rrextust.b 𝐵 = (Base‘𝑅)
rrextust.d 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
Assertion
Ref Expression
rrextust (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷))

Proof of Theorem rrextust
StepHypRef Expression
1 rrextust.b . . . 4 𝐵 = (Base‘𝑅)
2 rrextust.d . . . 4 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
3 eqid 2801 . . . 4 (ℤMod‘𝑅) = (ℤMod‘𝑅)
41, 2, 3isrrext 31349 . . 3 (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
54simp3bi 1144 . 2 (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))
65simprd 499 1 (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112   × cxp 5521  cres 5525  cfv 6328  0cc0 10530  Basecbs 16478  distcds 16569  DivRingcdr 19498  metUnifcmetu 20085  ℤModczlm 20197  chrcchr 20198  UnifStcuss 22862  CUnifSpccusp 22906  NrmRingcnrg 23189  NrmModcnlm 23190   ℝExt crrext 31343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-xp 5529  df-res 5535  df-iota 6287  df-fv 6336  df-rrext 31348
This theorem is referenced by:  rrhfe  31361  rrhcne  31362  sitgclg  31708
  Copyright terms: Public domain W3C validator