Metamath Proof Explorer

Theorem fucolid

Description: Post-compose a natural transformation with an identity natural transformation. (Contributed by Zhi Wang, 11-Oct-2025)

Ref Expression
Hypotheses fucolid.p 
|- ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P )
fucolid.i 
|- I = ( Id ` Q )
fucolid.q 
|- Q = ( D FuncCat E )
fucolid.a 
|- ( ph -> A e. ( G ( C Nat D ) H ) )
fucolid.f 
|- ( ph -> F e. ( D Func E ) )
Assertion fucolid 
|- ( ph -> ( ( I ` F ) ( <. F , G >. P <. F , H >. ) A ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 fucolid.p 
 |-  ( ph -> ( 2nd ` ( <. C , D >. o.F E ) ) = P )
2 fucolid.i 
 |-  I = ( Id ` Q )
3 fucolid.q 
 |-  Q = ( D FuncCat E )
4 fucolid.a 
 |-  ( ph -> A e. ( G ( C Nat D ) H ) )
5 fucolid.f 
 |-  ( ph -> F e. ( D Func E ) )
6 eqid 
 |-  ( Id ` E ) = ( Id ` E )
7 3 2 6 5 fucid 
 |-  ( ph -> ( I ` F ) = ( ( Id ` E ) o. ( 1st ` F ) ) )
8 7 oveq1d 
 |-  ( ph -> ( ( I ` F ) ( <. F , G >. P <. F , H >. ) A ) = ( ( ( Id ` E ) o. ( 1st ` F ) ) ( <. F , G >. P <. F , H >. ) A ) )
9 eqid 
 |-  ( C Nat D ) = ( C Nat D )
10 9 4 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
11 9 10 natrcl2 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
12 11 funcrcl2 
 |-  ( ph -> C e. Cat )
13 11 funcrcl3 
 |-  ( ph -> D e. Cat )
14 5 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
15 14 funcrcl3 
 |-  ( ph -> E e. Cat )
16 eqidd 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
17 12 13 15 16 fucoelvv 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
18 1st2nd2 
 |-  ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
19 17 18 syl 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
20 1 opeq2d 
 |-  ( ph -> <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. )
21 19 20 eqtrd 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , P >. )
22 eqidd 
 |-  ( ph -> <. F , G >. = <. F , G >. )
23 eqidd 
 |-  ( ph -> <. F , H >. = <. F , H >. )
24 eqid 
 |-  ( D Nat E ) = ( D Nat E )
25 3 24 6 5 fucidcl 
 |-  ( ph -> ( ( Id ` E ) o. ( 1st ` F ) ) e. ( F ( D Nat E ) F ) )
26 21 22 23 4 25 fuco22a 
 |-  ( ph -> ( ( ( Id ` E ) o. ( 1st ` F ) ) ( <. F , G >. P <. F , H >. ) A ) = ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. ( 1st ` F ) ) ` ( ( 1st ` H ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) ) )
27 eqid 
 |-  ( Base ` D ) = ( Base ` D )
28 eqid 
 |-  ( Base ` E ) = ( Base ` E )
29 14 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
30 27 28 29 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) : ( Base ` D ) --> ( Base ` E ) )
31 eqid 
 |-  ( Base ` C ) = ( Base ` C )
32 9 10 natrcl3 
 |-  ( ph -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
33 31 27 32 funcf1 
 |-  ( ph -> ( 1st ` H ) : ( Base ` C ) --> ( Base ` D ) )
34 33 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` H ) ` x ) e. ( Base ` D ) )
35 30 34 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( Id ` E ) o. ( 1st ` F ) ) ` ( ( 1st ` H ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) )
36 35 oveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( Id ` E ) o. ( 1st ` F ) ) ` ( ( 1st ` H ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) = ( ( ( Id ` E ) ` ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )
37 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
38 15 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
39 31 27 11 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
40 39 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
41 30 40 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) e. ( Base ` E ) )
42 eqid 
 |-  ( comp ` E ) = ( comp ` E )
43 30 34 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) e. ( Base ` E ) )
44 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
45 27 44 37 29 40 34 funcf2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) : ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) --> ( ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) )
46 10 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> A e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
47 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
48 9 46 31 44 47 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
49 45 48 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) )
50 28 37 6 38 41 42 43 49 catlid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( Id ` E ) ` ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) )
51 36 50 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( Id ` E ) o. ( 1st ` F ) ) ` ( ( 1st ` H ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) )
52 51 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. ( 1st ` F ) ) ` ( ( 1st ` H ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` H ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )
53 8 26 52 3eqtrd 
 |-  ( ph -> ( ( I ` F ) ( <. F , G >. P <. F , H >. ) A ) = ( x e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` H ) ` x ) ) ` ( A ` x ) ) ) )