Metamath Proof Explorer

Theorem fucorid

Description: Pre-composing a natural transformation with the identity natural transformation of a functor is pre-composing it with the object part of the functor, in maps-to notation. (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 )
fucorid.q 
|- Q = ( C FuncCat D )
fucorid.a 
|- ( ph -> A e. ( G ( D Nat E ) H ) )
fucorid.f 
|- ( ph -> F e. ( C Func D ) )
Assertion fucorid 
|- ( ph -> ( A ( <. G , F >. P <. H , F >. ) ( I ` F ) ) = ( x e. ( Base ` C ) |-> ( A ` ( ( 1st ` F ) ` x ) ) ) )

Proof

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