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 ⊢ abs ∘ − ∈ Met ⁡ ℂ

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 absf ⊢ abs : ℂ ⟶ ℝ
3 subf ⊢ − : ℂ × ℂ ⟶ ℂ
4 fco ⊢ abs : ℂ ⟶ ℝ ∧ − : ℂ × ℂ ⟶ ℂ → abs ∘ − : ℂ × ℂ ⟶ ℝ
5 2 3 4 mp2an ⊢ abs ∘ − : ℂ × ℂ ⟶ ℝ
6 subcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y ∈ ℂ
7 6 abs00ad ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = 0 ↔ x − y = 0
8 eqid ⊢ abs ∘ − = abs ∘ −
9 8 cnmetdval ⊢ x ∈ ℂ ∧ y ∈ ℂ → x abs ∘ − y = x − y
10 9 eqcomd ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = x abs ∘ − y
11 10 eqeq1d ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = 0 ↔ x abs ∘ − y = 0
12 subeq0 ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = 0 ↔ x = y
13 7 11 12 3bitr3d ⊢ x ∈ ℂ ∧ y ∈ ℂ → x abs ∘ − y = 0 ↔ x = y
14 abs3dif ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x − y ≤ x − z + z − y
15 abssub ⊢ x ∈ ℂ ∧ z ∈ ℂ → x − z = z − x
16 15 oveq1d ⊢ x ∈ ℂ ∧ z ∈ ℂ → x − z + z − y = z − x + z − y
17 16 3adant2 ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x − z + z − y = z − x + z − y
18 14 17 breqtrd ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x − y ≤ z − x + z − y
19 9 3adant3 ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x abs ∘ − y = x − y
20 8 cnmetdval ⊢ z ∈ ℂ ∧ x ∈ ℂ → z abs ∘ − x = z − x
21 20 3adant3 ⊢ z ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ → z abs ∘ − x = z − x
22 8 cnmetdval ⊢ z ∈ ℂ ∧ y ∈ ℂ → z abs ∘ − y = z − y
23 22 3adant2 ⊢ z ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ → z abs ∘ − y = z − y
24 21 23 oveq12d ⊢ z ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ → z abs ∘ − x + z abs ∘ − y = z − x + z − y
25 24 3coml ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → z abs ∘ − x + z abs ∘ − y = z − x + z − y
26 18 19 25 3brtr4d ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x abs ∘ − y ≤ z abs ∘ − x + z abs ∘ − y
27 1 5 13 26 ismeti ⊢ abs ∘ − ∈ Met ⁡ ℂ