Theorem rrextcusp 34002

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 2730	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2730	. . . 4 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3		eqid 2730	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 33997	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
5	4	simp3bi 1147	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))))
6	5	simpld 494	1 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   × cxp 5639   ↾ cres 5643  ‘cfv 6514  0cc0 11075  Basecbs 17186  distcds 17236  DivRingcdr 20645  metUnifcmetu 21262  ℤModczlm 21417  chrcchr 21418  UnifStcuss 24148  CUnifSpccusp 24191  NrmRingcnrg 24474  NrmModcnlm 24475   ℝExt crrext 33991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653  df-iota 6467  df-fv 6522  df-rrext 33996

This theorem is referenced by:  rrhfe  34009  rrhcne  34010  sitgclg  34340