Metamath Proof Explorer

Theorem postcof2

Description: A component of the action of a post-composition functor is obtained by applying the morphism part of F to the component morphism. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses postcof1st.q 
|- Q = ( C FuncCat D )
postcof1st.r 
|- R = ( D FuncCat E )
postcof1st.o 
|- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
postcof1st.f 
|- ( ph -> F e. ( D Func E ) )
postcof1st.c 
|- ( ph -> C e. Cat )
postcof1st.k 
|- K = ( ( 1st ` .o. ) ` F )
postcof2.g 
|- ( ph -> G e. ( C Func D ) )
postcof2.h 
|- ( ph -> H e. ( C Func D ) )
postcof2.a 
|- ( ph -> A e. ( G ( C Nat D ) H ) )
postcof2.x 
|- ( ph -> X e. ( Base ` C ) )
Assertion postcof2 
|- ( ph -> ( ( ( G ( 2nd ` K ) H ) ` A ) ` X ) = ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` H ) ` X ) ) ` ( A ` X ) ) )

Proof

Step Hyp Ref Expression
1 postcof1st.q 
 |-  Q = ( C FuncCat D )
2 postcof1st.r 
 |-  R = ( D FuncCat E )
3 postcof1st.o 
 |-  .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) )
4 postcof1st.f 
 |-  ( ph -> F e. ( D Func E ) )
5 postcof1st.c 
 |-  ( ph -> C e. Cat )
6 postcof1st.k 
 |-  K = ( ( 1st ` .o. ) ` F )
7 postcof2.g 
 |-  ( ph -> G e. ( C Func D ) )
8 postcof2.h 
 |-  ( ph -> H e. ( C Func D ) )
9 postcof2.a 
 |-  ( ph -> A e. ( G ( C Nat D ) H ) )
10 postcof2.x 
 |-  ( ph -> X e. ( Base ` C ) )
11 1 2 3 4 5 6 postcof2nd 
 |-  ( ph -> ( 2nd ` K ) = ( g e. ( C Func D ) , h e. ( C Func D ) |-> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) ) )
12 simprl 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> g = G )
13 simprr 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> h = H )
14 12 13 oveq12d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( g ( C Nat D ) h ) = ( G ( C Nat D ) H ) )
15 12 fveq2d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( 1st ` g ) = ( 1st ` G ) )
16 15 fveq1d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( ( 1st ` g ) ` x ) = ( ( 1st ` G ) ` x ) )
17 13 fveq2d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( 1st ` h ) = ( 1st ` H ) )
18 17 fveq1d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( ( 1st ` h ) ` x ) = ( ( 1st ` H ) ` x ) )
19 16 18 oveq12d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) = ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) )
20 19 fveq1d 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) )
21 20 mpteq2dv 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) )
22 14 21 mpteq12dv 
 |-  ( ( ph /\ ( g = G /\ h = H ) ) -> ( a e. ( g ( C Nat D ) h ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` g ) ` x ) ( 2nd ` F ) ( ( 1st ` h ) ` x ) ) ` ( a ` x ) ) ) ) = ( a e. ( G ( C Nat D ) H ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) ) )
23 ovex 
 |-  ( G ( C Nat D ) H ) e. _V
24 23 mptex 
 |-  ( a e. ( G ( C Nat D ) H ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) ) e. _V
25 24 a1i 
 |-  ( ph -> ( a e. ( G ( C Nat D ) H ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) ) e. _V )
26 11 22 7 8 25 ovmpod 
 |-  ( ph -> ( G ( 2nd ` K ) H ) = ( a e. ( G ( C Nat D ) H ) |-> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) ) )
27 simpr 
 |-  ( ( ph /\ a = A ) -> a = A )
28 27 fveq1d 
 |-  ( ( ph /\ a = A ) -> ( a ` x ) = ( A ` x ) )
29 28 fveq2d 
 |-  ( ( ph /\ a = A ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) )
30 29 mpteq2dv 
 |-  ( ( ph /\ a = A ) -> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( a ` x ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )
31 fvex 
 |-  ( Base ` C ) e. _V
32 31 mptex 
 |-  ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) e. _V
33 32 a1i 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) e. _V )
34 26 30 9 33 fvmptd 
 |-  ( ph -> ( ( G ( 2nd ` K ) H ) ` A ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )
35 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
36 35 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` X ) )
37 35 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` H ) ` x ) = ( ( 1st ` H ) ` X ) )
38 36 37 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) = ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` H ) ` X ) ) )
39 35 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( A ` x ) = ( A ` X ) )
40 38 39 fveq12d 
 |-  ( ( ph /\ x = X ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) = ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` H ) ` X ) ) ` ( A ` X ) ) )
41 fvexd 
 |-  ( ph -> ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` H ) ` X ) ) ` ( A ` X ) ) e. _V )
42 34 40 10 41 fvmptd 
 |-  ( ph -> ( ( ( G ( 2nd ` K ) H ) ` A ) ` X ) = ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` H ) ` X ) ) ` ( A ` X ) ) )