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 30393
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 2771 . . . 4 (ℤMod‘𝑅) = (ℤMod‘𝑅)
41, 2, 3isrrext 30385 . . 3 (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
54simp3bi 1141 . 2 (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))
65simprd 479 1 (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145   × cxp 5248  cres 5252  cfv 6032  0cc0 10139  Basecbs 16065  distcds 16159  DivRingcdr 18958  metUnifcmetu 19953  ℤModczlm 20065  chrcchr 20066  UnifStcuss 22278  CUnifSpccusp 22322  NrmRingcnrg 22605  NrmModcnlm 22606   ℝExt crrext 30379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-xp 5256  df-res 5262  df-iota 5995  df-fv 6040  df-rrext 30384
This theorem is referenced by:  rrhfe  30397  rrhcne  30398  sitgclg  30745
  Copyright terms: Public domain W3C validator