# 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 ${⊢}{\phi }\to {F}:{X}⟶{V}×{W}$
fvovco.2 ${⊢}{\phi }\to {Y}\in {X}$
Assertion fvovco ${⊢}{\phi }\to \left({O}\circ {F}\right)\left({Y}\right)={1}^{st}\left({F}\left({Y}\right)\right){O}{2}^{nd}\left({F}\left({Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fvovco.1 ${⊢}{\phi }\to {F}:{X}⟶{V}×{W}$
2 fvovco.2 ${⊢}{\phi }\to {Y}\in {X}$
3 1 2 ffvelrnd ${⊢}{\phi }\to {F}\left({Y}\right)\in \left({V}×{W}\right)$
4 1st2nd2 ${⊢}{F}\left({Y}\right)\in \left({V}×{W}\right)\to {F}\left({Y}\right)=⟨{1}^{st}\left({F}\left({Y}\right)\right),{2}^{nd}\left({F}\left({Y}\right)\right)⟩$
5 3 4 syl ${⊢}{\phi }\to {F}\left({Y}\right)=⟨{1}^{st}\left({F}\left({Y}\right)\right),{2}^{nd}\left({F}\left({Y}\right)\right)⟩$
6 5 fveq2d ${⊢}{\phi }\to {O}\left({F}\left({Y}\right)\right)={O}\left(⟨{1}^{st}\left({F}\left({Y}\right)\right),{2}^{nd}\left({F}\left({Y}\right)\right)⟩\right)$
7 fvco3 ${⊢}\left({F}:{X}⟶{V}×{W}\wedge {Y}\in {X}\right)\to \left({O}\circ {F}\right)\left({Y}\right)={O}\left({F}\left({Y}\right)\right)$
8 1 2 7 syl2anc ${⊢}{\phi }\to \left({O}\circ {F}\right)\left({Y}\right)={O}\left({F}\left({Y}\right)\right)$
9 df-ov ${⊢}{1}^{st}\left({F}\left({Y}\right)\right){O}{2}^{nd}\left({F}\left({Y}\right)\right)={O}\left(⟨{1}^{st}\left({F}\left({Y}\right)\right),{2}^{nd}\left({F}\left({Y}\right)\right)⟩\right)$
10 9 a1i ${⊢}{\phi }\to {1}^{st}\left({F}\left({Y}\right)\right){O}{2}^{nd}\left({F}\left({Y}\right)\right)={O}\left(⟨{1}^{st}\left({F}\left({Y}\right)\right),{2}^{nd}\left({F}\left({Y}\right)\right)⟩\right)$
11 6 8 10 3eqtr4d ${⊢}{\phi }\to \left({O}\circ {F}\right)\left({Y}\right)={1}^{st}\left({F}\left({Y}\right)\right){O}{2}^{nd}\left({F}\left({Y}\right)\right)$