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∈ℂ→xabs∘−y=x−y
10 9 eqcomd ⊢x∈ℂ∧y∈ℂ→x−y=xabs∘−y
11 10 eqeq1d ⊢x∈ℂ∧y∈ℂ→x−y=0↔xabs∘−y=0
12 subeq0 ⊢x∈ℂ∧y∈ℂ→x−y=0↔x=y
13 7 11 12 3bitr3d ⊢x∈ℂ∧y∈ℂ→xabs∘−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∈ℂ→xabs∘−y=x−y
20 8 cnmetdval ⊢z∈ℂ∧x∈ℂ→zabs∘−x=z−x
21 20 3adant3 ⊢z∈ℂ∧x∈ℂ∧y∈ℂ→zabs∘−x=z−x
22 8 cnmetdval ⊢z∈ℂ∧y∈ℂ→zabs∘−y=z−y
23 22 3adant2 ⊢z∈ℂ∧x∈ℂ∧y∈ℂ→zabs∘−y=z−y
24 21 23 oveq12d ⊢z∈ℂ∧x∈ℂ∧y∈ℂ→zabs∘−x+zabs∘−y=z−x+z−y
25 24 3coml ⊢x∈ℂ∧y∈ℂ∧z∈ℂ→zabs∘−x+zabs∘−y=z−x+z−y
26 18 19 25 3brtr4d ⊢x∈ℂ∧y∈ℂ∧z∈ℂ→xabs∘−y≤zabs∘−x+zabs∘−y
27 1 5 13 26 ismeti ⊢abs∘−∈Met⁡ℂ