Metamath Proof Explorer


Theorem cnims

Description: The metric induced on the complex numbers. cnmet proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006) (Revised by NM, 15-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses cnims.6
|- U = <. <. + , x. >. , abs >.
cnims.7
|- D = ( abs o. - )
Assertion cnims
|- D = ( IndMet ` U )

Proof

Step Hyp Ref Expression
1 cnims.6
 |-  U = <. <. + , x. >. , abs >.
2 cnims.7
 |-  D = ( abs o. - )
3 1 cnnv
 |-  U e. NrmCVec
4 1 cnnvm
 |-  - = ( -v ` U )
5 1 cnnvnm
 |-  abs = ( normCV ` U )
6 eqid
 |-  ( IndMet ` U ) = ( IndMet ` U )
7 4 5 6 imsval
 |-  ( U e. NrmCVec -> ( IndMet ` U ) = ( abs o. - ) )
8 3 7 ax-mp
 |-  ( IndMet ` U ) = ( abs o. - )
9 2 8 eqtr4i
 |-  D = ( IndMet ` U )