This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
7 6 abs00ad ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) = 0 ↔ ( 𝑥 − 𝑦 ) = 0 ) )
8 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
9 8 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
10 9 eqcomd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( 𝑥 ( abs ∘ − ) 𝑦 ) )
11 10 eqeq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) = 0 ↔ ( 𝑥 ( abs ∘ − ) 𝑦 ) = 0 ) )
12 subeq0 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 − 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
13 7 11 12 3bitr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 ( abs ∘ − ) 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
14 abs3dif ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( abs ‘ ( 𝑥 − 𝑧 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
15 abssub ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
16 15 oveq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) = ( ( abs ‘ ( 𝑧 − 𝑥 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
17 16 3adant2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) = ( ( abs ‘ ( 𝑧 − 𝑥 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
18 14 17 breqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( abs ‘ ( 𝑧 − 𝑥 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
19 9 3adant3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
20 8 cnmetdval ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
21 20 3adant3 ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
22 8 cnmetdval ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
23 22 3adant2 ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
24 21 23 oveq12d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑧 ( abs ∘ − ) 𝑥 ) + ( 𝑧 ( abs ∘ − ) 𝑦 ) ) = ( ( abs ‘ ( 𝑧 − 𝑥 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
25 24 3coml ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ( abs ∘ − ) 𝑥 ) + ( 𝑧 ( abs ∘ − ) 𝑦 ) ) = ( ( abs ‘ ( 𝑧 − 𝑥 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
26 18 19 25 3brtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) ≤ ( ( 𝑧 ( abs ∘ − ) 𝑥 ) + ( 𝑧 ( abs ∘ − ) 𝑦 ) ) )
27 1 5 13 26 ismeti ⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )