Theorem rrextust 34342

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

Step	Hyp	Ref	Expression
1		rrextust.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
2		rrextust.d	. . . 4 ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵))
3		eqid 2769	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 34334	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
5	4	simp3bi 1163	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))
6	5	simprd 500	1 ⊢ (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   × cxp 5660   ↾ cres 5664  ‘cfv 6537  0cc0 11099  Basecbs 17268  distcds 17318  DivRingcdr 20812  metUnifcmetu 21481  ℤModczlm 21618  chrcchr 21619  UnifStcuss 24378  CUnifSpccusp 24421  NrmRingcnrg 24704  NrmModcnlm 24705   ℝExt crrext 34328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-res 5674  df-iota 6493  df-fv 6545  df-rrext 34333

This theorem is referenced by:  rrhfe  34346  rrhcne  34347  sitgclg  34676