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