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	ffvelrnd	|- ( 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 ) ) ) ) )