Theorem opco1

Description: Value of an operation precomposed with the projection on the first component. (Contributed by Mario Carneiro, 28-May-2014) Generalize to closed form. (Revised by BJ, 27-Oct-2024)

	Ref	Expression
Hypotheses	opco1.exa	$$⊢\phi \to A\in V$$
	opco1.exb	$$⊢\phi \to B\in W$$
Assertion	opco1	$$⊢\phi \to A\left(F\circ 1^{st}\right)B=F\left(A\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 1^{st}\right)B=\left(F\circ 1^{st}\right)\left(⟨A,B⟩\right)$$
4	3	a1i	$$⊢\phi \to A\left(F\circ 1^{st}\right)B=\left(F\circ 1^{st}\right)\left(⟨A,B⟩\right)$$
5		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
6		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
7	5 6	mp1i	$$⊢\phi \to 1^{st}:\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 1^{st}\right)\left(⟨A,B⟩\right)=F\left(1^{st}\left(⟨A,B⟩\right)\right)$$
11		op1stg	$$⊢\left(A\in V\wedge B\in W\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
12	1 2 11	syl2anc	$$⊢\phi \to 1^{st}\left(⟨A,B⟩\right)=A$$
13	12	fveq2d	$$⊢\phi \to F\left(1^{st}\left(⟨A,B⟩\right)\right)=F\left(A\right)$$
14	4 10 13	3eqtrd	$$⊢\phi \to A\left(F\circ 1^{st}\right)B=F\left(A\right)$$