Metamath Proof Explorer

Theorem cnfldds

Description: The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldds 
|- ( abs o. - ) = ( dist ` CCfld )

Proof

Step Hyp Ref Expression
1 absf 
 |-  abs : CC --> RR
2 subf 
 |-  - : ( CC X. CC ) --> CC
3 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
4 1 2 3 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
5 cnex 
 |-  CC e. _V
6 5 5 xpex 
 |-  ( CC X. CC ) e. _V
7 reex 
 |-  RR e. _V
8 fex2 
 |-  ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ ( CC X. CC ) e. _V /\ RR e. _V ) -> ( abs o. - ) e. _V )
9 4 6 7 8 mp3an 
 |-  ( abs o. - ) e. _V
10 cnfldstr 
 |-  CCfld Struct <. 1 , ; 1 3 >.
11 dsid 
 |-  dist = Slot ( dist ` ndx )
12 snsstp3 
 |-  { <. ( dist ` ndx ) , ( abs o. - ) >. } C_ { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
13 ssun1 
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } C_ ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
14 ssun2 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
15 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
16 14 15 sseqtrri 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) C_ CCfld
17 13 16 sstri 
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } C_ CCfld
18 12 17 sstri 
 |-  { <. ( dist ` ndx ) , ( abs o. - ) >. } C_ CCfld
19 10 11 18 strfv 
 |-  ( ( abs o. - ) e. _V -> ( abs o. - ) = ( dist ` CCfld ) )
20 9 19 ax-mp 
 |-  ( abs o. - ) = ( dist ` CCfld )