# Metamath Proof Explorer

## Theorem cnmet

Description: The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006)

Ref Expression
Assertion cnmet ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
3 subf ${⊢}-:ℂ×ℂ⟶ℂ$
4 fco ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ×ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
5 2 3 4 mp2an ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
6 subcl ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}-{y}\in ℂ$
7 6 abs00ad ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left(\left|{x}-{y}\right|=0↔{x}-{y}=0\right)$
8 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
9 8 cnmetdval ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}\left(\mathrm{abs}\circ -\right){y}=\left|{x}-{y}\right|$
10 9 eqcomd ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left|{x}-{y}\right|={x}\left(\mathrm{abs}\circ -\right){y}$
11 10 eqeq1d ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left(\left|{x}-{y}\right|=0↔{x}\left(\mathrm{abs}\circ -\right){y}=0\right)$
12 subeq0 ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left({x}-{y}=0↔{x}={y}\right)$
13 7 11 12 3bitr3d ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left({x}\left(\mathrm{abs}\circ -\right){y}=0↔{x}={y}\right)$
14 abs3dif ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to \left|{x}-{y}\right|\le \left|{x}-{z}\right|+\left|{z}-{y}\right|$
15 abssub ${⊢}\left({x}\in ℂ\wedge {z}\in ℂ\right)\to \left|{x}-{z}\right|=\left|{z}-{x}\right|$
16 15 oveq1d ${⊢}\left({x}\in ℂ\wedge {z}\in ℂ\right)\to \left|{x}-{z}\right|+\left|{z}-{y}\right|=\left|{z}-{x}\right|+\left|{z}-{y}\right|$
17 16 3adant2 ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to \left|{x}-{z}\right|+\left|{z}-{y}\right|=\left|{z}-{x}\right|+\left|{z}-{y}\right|$
18 14 17 breqtrd ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to \left|{x}-{y}\right|\le \left|{z}-{x}\right|+\left|{z}-{y}\right|$
19 9 3adant3 ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to {x}\left(\mathrm{abs}\circ -\right){y}=\left|{x}-{y}\right|$
20 8 cnmetdval ${⊢}\left({z}\in ℂ\wedge {x}\in ℂ\right)\to {z}\left(\mathrm{abs}\circ -\right){x}=\left|{z}-{x}\right|$
21 20 3adant3 ${⊢}\left({z}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℂ\right)\to {z}\left(\mathrm{abs}\circ -\right){x}=\left|{z}-{x}\right|$
22 8 cnmetdval ${⊢}\left({z}\in ℂ\wedge {y}\in ℂ\right)\to {z}\left(\mathrm{abs}\circ -\right){y}=\left|{z}-{y}\right|$
23 22 3adant2 ${⊢}\left({z}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℂ\right)\to {z}\left(\mathrm{abs}\circ -\right){y}=\left|{z}-{y}\right|$
24 21 23 oveq12d ${⊢}\left({z}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℂ\right)\to \left({z}\left(\mathrm{abs}\circ -\right){x}\right)+\left({z}\left(\mathrm{abs}\circ -\right){y}\right)=\left|{z}-{x}\right|+\left|{z}-{y}\right|$
25 24 3coml ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to \left({z}\left(\mathrm{abs}\circ -\right){x}\right)+\left({z}\left(\mathrm{abs}\circ -\right){y}\right)=\left|{z}-{x}\right|+\left|{z}-{y}\right|$
26 18 19 25 3brtr4d ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {z}\in ℂ\right)\to {x}\left(\mathrm{abs}\circ -\right){y}\le \left({z}\left(\mathrm{abs}\circ -\right){x}\right)+\left({z}\left(\mathrm{abs}\circ -\right){y}\right)$
27 1 5 13 26 ismeti ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$