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 | ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩ | |
| cnims.7 | ⊢ 𝐷 = ( abs ∘ − ) | ||
| Assertion | cnims | ⊢ 𝐷 = ( IndMet ‘ 𝑈 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnims.6 | ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩ | |
| 2 | cnims.7 | ⊢ 𝐷 = ( abs ∘ − ) | |
| 3 | 1 | cnnv | ⊢ 𝑈 ∈ NrmCVec |
| 4 | 1 | cnnvm | ⊢ − = ( −𝑣 ‘ 𝑈 ) |
| 5 | 1 | cnnvnm | ⊢ abs = ( normCV ‘ 𝑈 ) |
| 6 | eqid | ⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 ) | |
| 7 | 4 5 6 | imsval | ⊢ ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) = ( abs ∘ − ) ) |
| 8 | 3 7 | ax-mp | ⊢ ( IndMet ‘ 𝑈 ) = ( abs ∘ − ) |
| 9 | 2 8 | eqtr4i | ⊢ 𝐷 = ( IndMet ‘ 𝑈 ) |