Metamath Proof Explorer

Theorem cnflduss

Description: The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Hypothesis cnflduss.1 
|- U = ( UnifSt ` CCfld )
Assertion cnflduss 
|- U = ( metUnif ` ( abs o. - ) )

Proof

Step Hyp Ref Expression
1 cnflduss.1 
 |-  U = ( UnifSt ` CCfld )
2 0cn 
 |-  0 e. CC
3 2 ne0ii 
 |-  CC =/= (/)
4 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
5 xmetpsmet 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( abs o. - ) e. ( PsMet ` CC ) )
6 4 5 ax-mp 
 |-  ( abs o. - ) e. ( PsMet ` CC )
7 metuust 
 |-  ( ( CC =/= (/) /\ ( abs o. - ) e. ( PsMet ` CC ) ) -> ( metUnif ` ( abs o. - ) ) e. ( UnifOn ` CC ) )
8 3 6 7 mp2an 
 |-  ( metUnif ` ( abs o. - ) ) e. ( UnifOn ` CC )
9 ustuni 
 |-  ( ( metUnif ` ( abs o. - ) ) e. ( UnifOn ` CC ) -> U. ( metUnif ` ( abs o. - ) ) = ( CC X. CC ) )
10 8 9 ax-mp 
 |-  U. ( metUnif ` ( abs o. - ) ) = ( CC X. CC )
11 10 eqcomi 
 |-  ( CC X. CC ) = U. ( metUnif ` ( abs o. - ) )
12 cnfldbas 
 |-  CC = ( Base ` CCfld )
13 cnfldunif 
 |-  ( metUnif ` ( abs o. - ) ) = ( UnifSet ` CCfld )
14 12 13 ussid 
 |-  ( ( CC X. CC ) = U. ( metUnif ` ( abs o. - ) ) -> ( metUnif ` ( abs o. - ) ) = ( UnifSt ` CCfld ) )
15 11 14 ax-mp 
 |-  ( metUnif ` ( abs o. - ) ) = ( UnifSt ` CCfld )
16 1 15 eqtr4i 
 |-  U = ( metUnif ` ( abs o. - ) )