Metamath Proof Explorer

Theorem fuco23

Description: The morphism part of the functor composition bifunctor. See also fuco23a . (Contributed by Zhi Wang, 29-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 fuco22.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco22.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
3 fuco22.v 
 |-  ( ph -> V = <. <. R , S >. , <. M , N >. >. )
4 fuco22.a 
 |-  ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
5 fuco22.b 
 |-  ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
6 fuco23.x 
 |-  ( ph -> X e. ( Base ` C ) )
7 fuco23.o 
 |-  ( ph -> .* = ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
8 1 2 3 4 5 fuco22 
 |-  ( ph -> ( B ( U P V ) A ) = ( x e. ( Base ` C ) |-> ( ( B ` ( M ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) ) ) )
9 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
10 9 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( F ` x ) = ( F ` X ) )
11 10 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( K ` ( F ` x ) ) = ( K ` ( F ` X ) ) )
12 9 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( M ` x ) = ( M ` X ) )
13 12 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( K ` ( M ` x ) ) = ( K ` ( M ` X ) ) )
14 11 13 opeq12d 
 |-  ( ( ph /\ x = X ) -> <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. = <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. )
15 12 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( R ` ( M ` x ) ) = ( R ` ( M ` X ) ) )
16 14 15 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) = ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
17 7 adantr 
 |-  ( ( ph /\ x = X ) -> .* = ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) )
18 16 17 eqtr4d 
 |-  ( ( ph /\ x = X ) -> ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) = .* )
19 12 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( B ` ( M ` x ) ) = ( B ` ( M ` X ) ) )
20 10 12 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( F ` x ) L ( M ` x ) ) = ( ( F ` X ) L ( M ` X ) ) )
21 9 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( A ` x ) = ( A ` X ) )
22 20 21 fveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) = ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) )
23 18 19 22 oveq123d 
 |-  ( ( ph /\ x = X ) -> ( ( B ` ( M ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) ) = ( ( B ` ( M ` X ) ) .* ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) )
24 ovexd 
 |-  ( ph -> ( ( B ` ( M ` X ) ) .* ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) e. _V )
25 8 23 6 24 fvmptd 
 |-  ( ph -> ( ( B ( U P V ) A ) ` X ) = ( ( B ` ( M ` X ) ) .* ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) )