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