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 ‘ ℂ )