This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldcusp

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

Ref Expression
Assertion cnfldcusp 
|- CCfld e. CUnifSp

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 1 ne0ii 
 |-  CC =/= (/)
3 cncms 
 |-  CCfld e. CMetSp
4 eqid 
 |-  ( UnifSt ` CCfld ) = ( UnifSt ` CCfld )
5 4 cnflduss 
 |-  ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) )
6 cnfldbas 
 |-  CC = ( Base ` CCfld )
7 absf 
 |-  abs : CC --> RR
8 subf 
 |-  - : ( CC X. CC ) --> CC
9 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
10 7 8 9 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
11 ffn 
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
12 fnresdm 
 |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )
13 10 11 12 mp2b 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )
14 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
15 14 reseq1i 
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
16 13 15 eqtr3i 
 |-  ( abs o. - ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )
17 6 16 4 cmetcusp1 
 |-  ( ( CC =/= (/) /\ CCfld e. CMetSp /\ ( UnifSt ` CCfld ) = ( metUnif ` ( abs o. - ) ) ) -> CCfld e. CUnifSp )
18 2 3 5 17 mp3an 
 |-  CCfld e. CUnifSp