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