Theorem fuco112xa

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. A morphism is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fuco11.f	|- ( ph -> F ( C Func D ) G )
	fuco11.k	|- ( ph -> K ( D Func E ) L )
	fuco11.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
	fuco111x.x	|- ( ph -> X e. ( Base ` C ) )
	fuco112x.y	|- ( ph -> Y e. ( Base ` C ) )
	fuco112xa.a	|- ( ph -> A e. ( X ( Hom ` C ) Y ) )
Assertion	fuco112xa	|- ( ph -> ( ( X ( 2nd ` ( O ` U ) ) Y ) ` A ) = ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2		fuco11.f	|- ( ph -> F ( C Func D ) G )
3		fuco11.k	|- ( ph -> K ( D Func E ) L )
4		fuco11.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5		fuco111x.x	|- ( ph -> X e. ( Base ` C ) )
6		fuco112x.y	|- ( ph -> Y e. ( Base ` C ) )
7		fuco112xa.a	|- ( ph -> A e. ( X ( Hom ` C ) Y ) )
8	1 2 3 4 5 6	fuco112x	|- ( ph -> ( X ( 2nd ` ( O ` U ) ) Y ) = ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) )
9	8	fveq1d	|- ( ph -> ( ( X ( 2nd ` ( O ` U ) ) Y ) ` A ) = ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` A ) )
10		eqid	|- ( Base ` C ) = ( Base ` C )
11		eqid	|- ( Hom ` C ) = ( Hom ` C )
12		eqid	|- ( Hom ` D ) = ( Hom ` D )
13	10 11 12 2 5 6	funcf2	|- ( ph -> ( X G Y ) : ( X ( Hom ` C ) Y ) --> ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
14	13 7	fvco3d	|- ( ph -> ( ( ( ( F ` X ) L ( F ` Y ) ) o. ( X G Y ) ) ` A ) = ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` A ) ) )
15	9 14	eqtrd	|- ( ph -> ( ( X ( 2nd ` ( O ` U ) ) Y ) ` A ) = ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` A ) ) )