Theorem opco2

Description: Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024)

	Ref	Expression
Hypotheses	opco1.exa	$$⊢\phi \to A\in V$$
	opco1.exb	$$⊢\phi \to B\in W$$
Assertion	opco2	$$⊢\phi \to A\left(F\circ 2^{nd}\right)B=F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		opco1.exa	$$⊢\phi \to A\in V$$
2		opco1.exb	$$⊢\phi \to B\in W$$
3		df-ov	$$⊢A\left(F\circ 2^{nd}\right)B=\left(F\circ 2^{nd}\right)\left(⟨A,B⟩\right)$$
4	3	a1i	$$⊢\phi \to A\left(F\circ 2^{nd}\right)B=\left(F\circ 2^{nd}\right)\left(⟨A,B⟩\right)$$
5		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
6		fof	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 2^{nd}:\mathrm{V}⟶\mathrm{V}$$
7	5 6	mp1i	$$⊢\phi \to 2^{nd}:\mathrm{V}⟶\mathrm{V}$$
8		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to ⟨A,B⟩\in \mathrm{V}$$
10	7 9	fvco3d	$$⊢\phi \to \left(F\circ 2^{nd}\right)\left(⟨A,B⟩\right)=F\left(2^{nd}\left(⟨A,B⟩\right)\right)$$
11		op2ndg	$$⊢\left(A\in V\wedge B\in W\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
12	1 2 11	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨A,B⟩\right)=B$$
13	12	fveq2d	$$⊢\phi \to F\left(2^{nd}\left(⟨A,B⟩\right)\right)=F\left(B\right)$$
14	4 10 13	3eqtrd	$$⊢\phi \to A\left(F\circ 2^{nd}\right)B=F\left(B\right)$$