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 𝐷 = ( abs ∘ − )
cnmetcoval.f ( 𝜑𝐹 : 𝐴 ⟶ ( ℂ × ℂ ) )
cnmetcoval.b ( 𝜑𝐵𝐴 )
Assertion cnmetcoval ( 𝜑 → ( ( 𝐷𝐹 ) ‘ 𝐵 ) = ( abs ‘ ( ( 1st ‘ ( 𝐹𝐵 ) ) − ( 2nd ‘ ( 𝐹𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnmetcoval.d 𝐷 = ( abs ∘ − )
2 cnmetcoval.f ( 𝜑𝐹 : 𝐴 ⟶ ( ℂ × ℂ ) )
3 cnmetcoval.b ( 𝜑𝐵𝐴 )
4 2 3 fvovco ( 𝜑 → ( ( 𝐷𝐹 ) ‘ 𝐵 ) = ( ( 1st ‘ ( 𝐹𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹𝐵 ) ) ) )
5 2 3 ffvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ( ℂ × ℂ ) )
6 xp1st ( ( 𝐹𝐵 ) ∈ ( ℂ × ℂ ) → ( 1st ‘ ( 𝐹𝐵 ) ) ∈ ℂ )
7 5 6 syl ( 𝜑 → ( 1st ‘ ( 𝐹𝐵 ) ) ∈ ℂ )
8 xp2nd ( ( 𝐹𝐵 ) ∈ ( ℂ × ℂ ) → ( 2nd ‘ ( 𝐹𝐵 ) ) ∈ ℂ )
9 5 8 syl ( 𝜑 → ( 2nd ‘ ( 𝐹𝐵 ) ) ∈ ℂ )
10 1 cnmetdval ( ( ( 1st ‘ ( 𝐹𝐵 ) ) ∈ ℂ ∧ ( 2nd ‘ ( 𝐹𝐵 ) ) ∈ ℂ ) → ( ( 1st ‘ ( 𝐹𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹𝐵 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹𝐵 ) ) − ( 2nd ‘ ( 𝐹𝐵 ) ) ) ) )
11 7 9 10 syl2anc ( 𝜑 → ( ( 1st ‘ ( 𝐹𝐵 ) ) 𝐷 ( 2nd ‘ ( 𝐹𝐵 ) ) ) = ( abs ‘ ( ( 1st ‘ ( 𝐹𝐵 ) ) − ( 2nd ‘ ( 𝐹𝐵 ) ) ) ) )
12 4 11 eqtrd ( 𝜑 → ( ( 𝐷𝐹 ) ‘ 𝐵 ) = ( abs ‘ ( ( 1st ‘ ( 𝐹𝐵 ) ) − ( 2nd ‘ ( 𝐹𝐵 ) ) ) ) )