Theorem rrextust 34114

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 2734	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 34106	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷))))
5	4	simp3bi 1147	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘𝐷)))
6	5	simprd 495	1 ⊢ (𝑅 ∈ ℝExt → (UnifSt‘𝑅) = (metUnif‘𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   × cxp 5620   ↾ cres 5624  ‘cfv 6490  0cc0 11024  Basecbs 17134  distcds 17184  DivRingcdr 20660  metUnifcmetu 21298  ℤModczlm 21453  chrcchr 21454  UnifStcuss 24195  CUnifSpccusp 24238  NrmRingcnrg 24521  NrmModcnlm 24522   ℝExt crrext 34100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634  df-iota 6446  df-fv 6498  df-rrext 34105

This theorem is referenced by:  rrhfe  34118  rrhcne  34119  sitgclg  34448