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	|- ( ph -> A e. V )
	opco1.exb	|- ( ph -> B e. W )
Assertion	opco1	|- ( ph -> ( A ( F o. 1st ) B ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		opco1.exa	|- ( ph -> A e. V )
2		opco1.exb	|- ( ph -> B e. W )
3		df-ov	|- ( A ( F o. 1st ) B ) = ( ( F o. 1st ) ` <. A , B >. )
4	3	a1i	|- ( ph -> ( A ( F o. 1st ) B ) = ( ( F o. 1st ) ` <. A , B >. ) )
5		fo1st	|- 1st : _V -onto-> _V
6		fof	|- ( 1st : _V -onto-> _V -> 1st : _V --> _V )
7	5 6	mp1i	|- ( ph -> 1st : _V --> _V )
8		opex	|- <. A , B >. e. _V
9	8	a1i	|- ( ph -> <. A , B >. e. _V )
10	7 9	fvco3d	|- ( ph -> ( ( F o. 1st ) ` <. A , B >. ) = ( F ` ( 1st ` <. A , B >. ) ) )
11		op1stg	|- ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )
12	1 2 11	syl2anc	|- ( ph -> ( 1st ` <. A , B >. ) = A )
13	12	fveq2d	|- ( ph -> ( F ` ( 1st ` <. A , B >. ) ) = ( F ` A ) )
14	4 10 13	3eqtrd	|- ( ph -> ( A ( F o. 1st ) B ) = ( F ` A ) )