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

Metamath Proof Explorer

Theorem fvovco

Description: Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses fvovco.1 
|- ( ph -> F : X --> ( V X. W ) )
fvovco.2 
|- ( ph -> Y e. X )
Assertion fvovco 
|- ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 fvovco.1 
 |-  ( ph -> F : X --> ( V X. W ) )
2 fvovco.2 
 |-  ( ph -> Y e. X )
3 1 2 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. ( V X. W ) )
4 1st2nd2 
 |-  ( ( F ` Y ) e. ( V X. W ) -> ( F ` Y ) = <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
5 3 4 syl 
 |-  ( ph -> ( F ` Y ) = <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
6 5 fveq2d 
 |-  ( ph -> ( O ` ( F ` Y ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. ) )
7 fvco3 
 |-  ( ( F : X --> ( V X. W ) /\ Y e. X ) -> ( ( O o. F ) ` Y ) = ( O ` ( F ` Y ) ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( ( O o. F ) ` Y ) = ( O ` ( F ` Y ) ) )
9 df-ov 
 |-  ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
10 9 a1i 
 |-  ( ph -> ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. ) )
11 6 8 10 3eqtr4d 
 |-  ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )