Theorem fuco23a

Description: The morphism part of the functor composition bifunctor. An alternate definition of o.F . See also fuco23 . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco23a.a	|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
	fuco23a.b	|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
	fuco23a.x	|- ( ph -> X e. ( Base ` C ) )
	fuco23a.p	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fuco23a.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
	fuco23a.v	|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
	fuco23a.o	|- ( ph -> .* = ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
Assertion	fuco23a	|- ( ph -> ( ( B ( U P V ) A ) ` X ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) .* ( B ` ( F ` X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco23a.a	|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
2		fuco23a.b	|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
3		fuco23a.x	|- ( ph -> X e. ( Base ` C ) )
4		fuco23a.p	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
5		fuco23a.u	|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
6		fuco23a.v	|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
7		fuco23a.o	|- ( ph -> .* = ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
8		eqid	|- ( comp ` E ) = ( comp ` E )
9	1 2 3 8	fuco23alem	|- ( ph -> ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( B ` ( F ` X ) ) ) )
10		eqidd	|- ( ph -> ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) = ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
11	4 5 6 1 2 3 10	fuco23	|- ( ph -> ( ( B ( U P V ) A ) ` X ) = ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) )
12	7	oveqd	|- ( ph -> ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) .* ( B ` ( F ` X ) ) ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( F ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( B ` ( F ` X ) ) ) )
13	9 11 12	3eqtr4d	|- ( ph -> ( ( B ( U P V ) A ) ` X ) = ( ( ( ( F ` X ) S ( M ` X ) ) ` ( A ` X ) ) .* ( B ` ( F ` X ) ) ) )