Metamath Proof Explorer

Theorem fuco22

Description: The morphism part of the functor composition bifunctor. See also fuco22a . (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 >. ) )
Assertion 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 ) ) ) ) )

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 eqid 
 |-  ( C Nat D ) = ( C Nat D )
7 6 4 natrcl2 
 |-  ( ph -> F ( C Func D ) G )
8 eqid 
 |-  ( D Nat E ) = ( D Nat E )
9 8 5 natrcl2 
 |-  ( ph -> K ( D Func E ) L )
10 6 4 natrcl3 
 |-  ( ph -> M ( C Func D ) N )
11 8 5 natrcl3 
 |-  ( ph -> R ( D Func E ) S )
12 1 7 9 2 10 11 3 fuco21 
 |-  ( ph -> ( U P V ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
13 simplrl 
 |-  ( ( ( ph /\ ( b = B /\ a = A ) ) /\ x e. ( Base ` C ) ) -> b = B )
14 13 fveq1d 
 |-  ( ( ( ph /\ ( b = B /\ a = A ) ) /\ x e. ( Base ` C ) ) -> ( b ` ( M ` x ) ) = ( B ` ( M ` x ) ) )
15 simplrr 
 |-  ( ( ( ph /\ ( b = B /\ a = A ) ) /\ x e. ( Base ` C ) ) -> a = A )
16 15 fveq1d 
 |-  ( ( ( ph /\ ( b = B /\ a = A ) ) /\ x e. ( Base ` C ) ) -> ( a ` x ) = ( A ` x ) )
17 16 fveq2d 
 |-  ( ( ( ph /\ ( b = B /\ a = A ) ) /\ x e. ( Base ` C ) ) -> ( ( ( F ` x ) L ( M ` x ) ) ` ( a ` x ) ) = ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) )
18 14 17 oveq12d 
 |-  ( ( ( ph /\ ( b = B /\ a = 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 ) ) ) = ( ( B ` ( M ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) ) )
19 18 mpteq2dva 
 |-  ( ( ph /\ ( b = B /\ a = 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 ) ) ) ) = ( 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 ) ) ) ) )
20 fvexd 
 |-  ( ph -> ( Base ` C ) e. _V )
21 20 mptexd 
 |-  ( ph -> ( 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 ) ) ) ) e. _V )
22 12 19 5 4 21 ovmpod 
 |-  ( 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 ) ) ) ) )