Theorem cnmetdval

Description: Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypothesis	cnmetdval.1	⊢ 𝐷 = ( abs ∘ − )
Assertion	cnmetdval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmetdval.1	⊢ 𝐷 = ( abs ∘ − )
2		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3		opelxpi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℂ × ℂ ) )
4		fvco3	⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
5	2 3 4	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
6		df-ov	⊢ ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7	1	fveq1i	⊢ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8	6 7	eqtri	⊢ ( 𝐴 𝐷 𝐵 ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
9		df-ov	⊢ ( 𝐴 − 𝐵 ) = ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ )
10	9	fveq2i	⊢ ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
11	5 8 10	3eqtr4g	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )