Metamath Proof Explorer

Theorem cnmet

Description: The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006)

Ref Expression
Assertion cnmet 
|- ( abs o. - ) e. ( Met ` CC )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 absf 
 |-  abs : CC --> RR
3 subf 
 |-  - : ( CC X. CC ) --> CC
4 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
5 2 3 4 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
6 subcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC )
7 6 abs00ad 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( abs ` ( x - y ) ) = 0 <-> ( x - y ) = 0 ) )
8 eqid 
 |-  ( abs o. - ) = ( abs o. - )
9 8 cnmetdval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( abs o. - ) y ) = ( abs ` ( x - y ) ) )
10 9 eqcomd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x - y ) ) = ( x ( abs o. - ) y ) )
11 10 eqeq1d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( abs ` ( x - y ) ) = 0 <-> ( x ( abs o. - ) y ) = 0 ) )
12 subeq0 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( x - y ) = 0 <-> x = y ) )
13 7 11 12 3bitr3d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( x ( abs o. - ) y ) = 0 <-> x = y ) )
14 abs3dif 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( abs ` ( x - y ) ) <_ ( ( abs ` ( x - z ) ) + ( abs ` ( z - y ) ) ) )
15 abssub 
 |-  ( ( x e. CC /\ z e. CC ) -> ( abs ` ( x - z ) ) = ( abs ` ( z - x ) ) )
16 15 oveq1d 
 |-  ( ( x e. CC /\ z e. CC ) -> ( ( abs ` ( x - z ) ) + ( abs ` ( z - y ) ) ) = ( ( abs ` ( z - x ) ) + ( abs ` ( z - y ) ) ) )
17 16 3adant2 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( abs ` ( x - z ) ) + ( abs ` ( z - y ) ) ) = ( ( abs ` ( z - x ) ) + ( abs ` ( z - y ) ) ) )
18 14 17 breqtrd 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( abs ` ( x - y ) ) <_ ( ( abs ` ( z - x ) ) + ( abs ` ( z - y ) ) ) )
19 9 3adant3 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( abs o. - ) y ) = ( abs ` ( x - y ) ) )
20 8 cnmetdval 
 |-  ( ( z e. CC /\ x e. CC ) -> ( z ( abs o. - ) x ) = ( abs ` ( z - x ) ) )
21 20 3adant3 
 |-  ( ( z e. CC /\ x e. CC /\ y e. CC ) -> ( z ( abs o. - ) x ) = ( abs ` ( z - x ) ) )
22 8 cnmetdval 
 |-  ( ( z e. CC /\ y e. CC ) -> ( z ( abs o. - ) y ) = ( abs ` ( z - y ) ) )
23 22 3adant2 
 |-  ( ( z e. CC /\ x e. CC /\ y e. CC ) -> ( z ( abs o. - ) y ) = ( abs ` ( z - y ) ) )
24 21 23 oveq12d 
 |-  ( ( z e. CC /\ x e. CC /\ y e. CC ) -> ( ( z ( abs o. - ) x ) + ( z ( abs o. - ) y ) ) = ( ( abs ` ( z - x ) ) + ( abs ` ( z - y ) ) ) )
25 24 3coml 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( z ( abs o. - ) x ) + ( z ( abs o. - ) y ) ) = ( ( abs ` ( z - x ) ) + ( abs ` ( z - y ) ) ) )
26 18 19 25 3brtr4d 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x ( abs o. - ) y ) <_ ( ( z ( abs o. - ) x ) + ( z ( abs o. - ) y ) ) )
27 1 5 13 26 ismeti 
 |-  ( abs o. - ) e. ( Met ` CC )