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 ) ) )