Theorem cnfldcusp

Description: The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

	Ref	Expression
Assertion	cnfldcusp	⊢ ℂfld ∈ CUnifSp

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2	1	ne0ii	⊢ ℂ ≠ ∅
3		cncms	⊢ ℂfld ∈ CMetSp
4		eqid	⊢ ( UnifSt ‘ ℂfld ) = ( UnifSt ‘ ℂfld )
5	4	cnflduss	⊢ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) )
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7		absf	⊢ abs : ℂ ⟶ ℝ
8		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
9		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
10	7 8 9	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
11		ffn	⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
12		fnresdm	⊢ ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
13	10 11 12	mp2b	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
14		cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
15	14	reseq1i	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
16	13 15	eqtr3i	⊢ ( abs ∘ − ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
17	6 16 4	cmetcusp1	⊢ ( ( ℂ ≠ ∅ ∧ ℂfld ∈ CMetSp ∧ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) ) ) → ℂfld ∈ CUnifSp )
18	2 3 5 17	mp3an	⊢ ℂfld ∈ CUnifSp