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

Metamath Proof Explorer

Theorem cnmetdval

Description: Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypothesis cnmetdval.1 
|- D = ( abs o. - )
Assertion cnmetdval 
|- ( ( A e. CC /\ B e. CC ) -> ( A D B ) = ( abs ` ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 cnmetdval.1 
 |-  D = ( abs o. - )
2 subf 
 |-  - : ( CC X. CC ) --> CC
3 opelxpi 
 |-  ( ( A e. CC /\ B e. CC ) -> <. A , B >. e. ( CC X. CC ) )
4 fvco3 
 |-  ( ( - : ( CC X. CC ) --> CC /\ <. A , B >. e. ( CC X. CC ) ) -> ( ( abs o. - ) ` <. A , B >. ) = ( abs ` ( - ` <. A , B >. ) ) )
5 2 3 4 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs o. - ) ` <. A , B >. ) = ( abs ` ( - ` <. A , B >. ) ) )
6 df-ov 
 |-  ( A D B ) = ( D ` <. A , B >. )
7 1 fveq1i 
 |-  ( D ` <. A , B >. ) = ( ( abs o. - ) ` <. A , B >. )
8 6 7 eqtri 
 |-  ( A D B ) = ( ( abs o. - ) ` <. A , B >. )
9 df-ov 
 |-  ( A - B ) = ( - ` <. A , B >. )
10 9 fveq2i 
 |-  ( abs ` ( A - B ) ) = ( abs ` ( - ` <. A , B >. ) )
11 5 8 10 3eqtr4g 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A D B ) = ( abs ` ( A - B ) ) )