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