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\times 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\times W$$
2		fvovco.2	$$⊢\phi \to Y\in X$$
3	1 2	ffvelrnd	$$⊢\phi \to F\left(Y\right)\in \left(V\times W\right)$$
4		1st2nd2	$$⊢F\left(Y\right)\in \left(V\times 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\times 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)$$