Theorem rrextcusp 31639

Description: An extension of ℝ is a complete uniform space. (Contributed by Thierry Arnoux, 2-May-2018.)

Assertion

Ref	Expression
rrextcusp	⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)

Proof of Theorem rrextcusp

Step	Hyp	Ref	Expression
1		eqid 2734	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2734	. . . 4 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3		eqid 2734	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 31634	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
5	4	simp3bi 1149	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))))
6	5	simpld 498	1 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   × cxp 5538   ↾ cres 5542  ‘cfv 6369  0cc0 10712  Basecbs 16684  distcds 16776  DivRingcdr 19739  metUnifcmetu 20326  ℤModczlm 20439  chrcchr 20440  UnifStcuss 23123  CUnifSpccusp 23166  NrmRingcnrg 23449  NrmModcnlm 23450   ℝExt crrext 31628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-rab 3063  df-v 3403  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-xp 5546  df-res 5552  df-iota 6327  df-fv 6377  df-rrext 31633

This theorem is referenced by:  rrhfe  31646  rrhcne  31647  sitgclg  31993