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 o. - )
cnmetcoval.f 
|- ( ph -> F : A --> ( CC X. CC ) )
cnmetcoval.b 
|- ( ph -> B e. A )
Assertion cnmetcoval 
|- ( ph -> ( ( D o. F ) ` B ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnmetcoval.d 
 |-  D = ( abs o. - )
2 cnmetcoval.f 
 |-  ( ph -> F : A --> ( CC X. CC ) )
3 cnmetcoval.b 
 |-  ( ph -> B e. A )
4 2 3 fvovco 
 |-  ( ph -> ( ( D o. F ) ` B ) = ( ( 1st ` ( F ` B ) ) D ( 2nd ` ( F ` B ) ) ) )
5 2 3 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. ( CC X. CC ) )
6 xp1st 
 |-  ( ( F ` B ) e. ( CC X. CC ) -> ( 1st ` ( F ` B ) ) e. CC )
7 5 6 syl 
 |-  ( ph -> ( 1st ` ( F ` B ) ) e. CC )
8 xp2nd 
 |-  ( ( F ` B ) e. ( CC X. CC ) -> ( 2nd ` ( F ` B ) ) e. CC )
9 5 8 syl 
 |-  ( ph -> ( 2nd ` ( F ` B ) ) e. CC )
10 1 cnmetdval 
 |-  ( ( ( 1st ` ( F ` B ) ) e. CC /\ ( 2nd ` ( F ` B ) ) e. CC ) -> ( ( 1st ` ( F ` B ) ) D ( 2nd ` ( F ` B ) ) ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )
11 7 9 10 syl2anc 
 |-  ( ph -> ( ( 1st ` ( F ` B ) ) D ( 2nd ` ( F ` B ) ) ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )
12 4 11 eqtrd 
 |-  ( ph -> ( ( D o. F ) ` B ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )