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