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

Metamath Proof Explorer

Theorem cnmetcoval

Description: Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses cnmetcoval.d ⊢ D = abs ∘ −
cnmetcoval.f ⊢ φ → F : A ⟶ ℂ × ℂ
cnmetcoval.b ⊢ φ → B ∈ A
Assertion cnmetcoval ⊢ φ → D ∘ F ⁡ B = 1 st ⁡ F ⁡ B − 2 nd ⁡ F ⁡ B

Proof

Step Hyp Ref Expression
1 cnmetcoval.d ⊢ D = abs ∘ −
2 cnmetcoval.f ⊢ φ → F : A ⟶ ℂ × ℂ
3 cnmetcoval.b ⊢ φ → B ∈ A
4 2 3 fvovco ⊢ φ → D ∘ F ⁡ B = 1 st ⁡ F ⁡ B D 2 nd ⁡ F ⁡ B
5 2 3 ffvelcdmd ⊢ φ → F ⁡ B ∈ ℂ × ℂ
6 xp1st ⊢ F ⁡ B ∈ ℂ × ℂ → 1 st ⁡ F ⁡ B ∈ ℂ
7 5 6 syl ⊢ φ → 1 st ⁡ F ⁡ B ∈ ℂ
8 xp2nd ⊢ F ⁡ B ∈ ℂ × ℂ → 2 nd ⁡ F ⁡ B ∈ ℂ
9 5 8 syl ⊢ φ → 2 nd ⁡ F ⁡ B ∈ ℂ
10 1 cnmetdval ⊢ 1 st ⁡ F ⁡ B ∈ ℂ ∧ 2 nd ⁡ F ⁡ B ∈ ℂ → 1 st ⁡ F ⁡ B D 2 nd ⁡ F ⁡ B = 1 st ⁡ F ⁡ B − 2 nd ⁡ F ⁡ B
11 7 9 10 syl2anc ⊢ φ → 1 st ⁡ F ⁡ B D 2 nd ⁡ F ⁡ B = 1 st ⁡ F ⁡ B − 2 nd ⁡ F ⁡ B
12 4 11 eqtrd ⊢ φ → D ∘ F ⁡ B = 1 st ⁡ F ⁡ B − 2 nd ⁡ F ⁡ B