Metamath Proof Explorer

Theorem prcofdiag

Description: A diagonal functor post-composed by a pre-composition functor is another diagonal functor. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses prcofdiag.l 
|- L = ( C DiagFunc D )
prcofdiag.m 
|- M = ( C DiagFunc E )
prcofdiag.f 
|- ( ph -> F e. ( E Func D ) )
prcofdiag.c 
|- ( ph -> C e. Cat )
prcofdiag.g 
|- ( ph -> ( <. D , C >. -o.F F ) = G )
Assertion prcofdiag 
|- ( ph -> ( G o.func L ) = M )

Proof

Step Hyp Ref Expression
1 prcofdiag.l 
 |-  L = ( C DiagFunc D )
2 prcofdiag.m 
 |-  M = ( C DiagFunc E )
3 prcofdiag.f 
 |-  ( ph -> F e. ( E Func D ) )
4 prcofdiag.c 
 |-  ( ph -> C e. Cat )
5 prcofdiag.g 
 |-  ( ph -> ( <. D , C >. -o.F F ) = G )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Base ` ( E FuncCat C ) ) = ( Base ` ( E FuncCat C ) )
8 3 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( E Func D ) ( 2nd ` F ) )
9 8 funcrcl3 
 |-  ( ph -> D e. Cat )
10 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
11 1 4 9 10 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
12 eqid 
 |-  ( E FuncCat C ) = ( E FuncCat C )
13 10 4 12 3 prcoffunca 
 |-  ( ph -> ( <. D , C >. -o.F F ) e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) )
14 5 13 eqeltrrd 
 |-  ( ph -> G e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) )
15 11 14 cofucl 
 |-  ( ph -> ( G o.func L ) e. ( C Func ( E FuncCat C ) ) )
16 15 func1st2nd 
 |-  ( ph -> ( 1st ` ( G o.func L ) ) ( C Func ( E FuncCat C ) ) ( 2nd ` ( G o.func L ) ) )
17 6 7 16 funcf1 
 |-  ( ph -> ( 1st ` ( G o.func L ) ) : ( Base ` C ) --> ( Base ` ( E FuncCat C ) ) )
18 17 ffnd 
 |-  ( ph -> ( 1st ` ( G o.func L ) ) Fn ( Base ` C ) )
19 8 funcrcl2 
 |-  ( ph -> E e. Cat )
20 2 4 19 12 diagcl 
 |-  ( ph -> M e. ( C Func ( E FuncCat C ) ) )
21 20 func1st2nd 
 |-  ( ph -> ( 1st ` M ) ( C Func ( E FuncCat C ) ) ( 2nd ` M ) )
22 6 7 21 funcf1 
 |-  ( ph -> ( 1st ` M ) : ( Base ` C ) --> ( Base ` ( E FuncCat C ) ) )
23 22 ffnd 
 |-  ( ph -> ( 1st ` M ) Fn ( Base ` C ) )
24 11 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> L e. ( C Func ( D FuncCat C ) ) )
25 14 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> G e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) )
26 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
27 6 24 25 26 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( G o.func L ) ) ` x ) = ( ( 1st ` G ) ` ( ( 1st ` L ) ` x ) ) )
28 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
29 9 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
30 eqid 
 |-  ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x )
31 1 28 29 6 26 30 diag1cl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` L ) ` x ) e. ( D Func C ) )
32 5 fveq2d 
 |-  ( ph -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) )
33 32 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) )
34 31 33 prcof1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` ( ( 1st ` L ) ` x ) ) = ( ( ( 1st ` L ) ` x ) o.func F ) )
35 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( E Func D ) )
36 1 2 35 28 6 26 prcofdiag1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` L ) ` x ) o.func F ) = ( ( 1st ` M ) ` x ) )
37 27 34 36 3eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( G o.func L ) ) ` x ) = ( ( 1st ` M ) ` x ) )
38 18 23 37 eqfnfvd 
 |-  ( ph -> ( 1st ` ( G o.func L ) ) = ( 1st ` M ) )
39 6 16 funcfn2 
 |-  ( ph -> ( 2nd ` ( G o.func L ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
40 6 21 funcfn2 
 |-  ( ph -> ( 2nd ` M ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
41 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
42 eqid 
 |-  ( Hom ` ( E FuncCat C ) ) = ( Hom ` ( E FuncCat C ) )
43 16 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( G o.func L ) ) ( C Func ( E FuncCat C ) ) ( 2nd ` ( G o.func L ) ) )
44 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
45 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
46 6 41 42 43 44 45 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( G o.func L ) ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` ( G o.func L ) ) ` x ) ( Hom ` ( E FuncCat C ) ) ( ( 1st ` ( G o.func L ) ) ` y ) ) )
47 46 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( G o.func L ) ) y ) Fn ( x ( Hom ` C ) y ) )
48 21 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` M ) ( C Func ( E FuncCat C ) ) ( 2nd ` M ) )
49 6 41 42 48 44 45 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` M ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` M ) ` x ) ( Hom ` ( E FuncCat C ) ) ( ( 1st ` M ) ` y ) ) )
50 49 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` M ) y ) Fn ( x ( Hom ` C ) y ) )
51 eqid 
 |-  ( Base ` E ) = ( Base ` E )
52 eqid 
 |-  ( Base ` D ) = ( Base ` D )
53 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> F e. ( E Func D ) )
54 53 func1st2nd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 1st ` F ) ( E Func D ) ( 2nd ` F ) )
55 51 52 54 funcf1 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 1st ` F ) : ( Base ` E ) --> ( Base ` D ) )
56 xpco2 
 |-  ( ( 1st ` F ) : ( Base ` E ) --> ( Base ` D ) -> ( ( ( Base ` D ) X. { f } ) o. ( 1st ` F ) ) = ( ( Base ` E ) X. { f } ) )
57 55 56 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( Base ` D ) X. { f } ) o. ( 1st ` F ) ) = ( ( Base ` E ) X. { f } ) )
58 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> L e. ( C Func ( D FuncCat C ) ) )
59 14 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> G e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) )
60 44 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
61 45 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
62 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
63 6 58 59 60 61 41 62 cofu2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( G o.func L ) ) y ) ` f ) = ( ( ( ( 1st ` L ) ` x ) ( 2nd ` G ) ( ( 1st ` L ) ` y ) ) ` ( ( x ( 2nd ` L ) y ) ` f ) ) )
64 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> C e. Cat )
65 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> D e. Cat )
66 1 6 52 41 64 65 60 61 62 diag2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` L ) y ) ` f ) = ( ( Base ` D ) X. { f } ) )
67 66 fveq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` L ) ` x ) ( 2nd ` G ) ( ( 1st ` L ) ` y ) ) ` ( ( x ( 2nd ` L ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) ( 2nd ` G ) ( ( 1st ` L ) ` y ) ) ` ( ( Base ` D ) X. { f } ) ) )
68 eqid 
 |-  ( D Nat C ) = ( D Nat C )
69 1 6 52 41 64 65 60 61 62 68 diag2cl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( Base ` D ) X. { f } ) e. ( ( ( 1st ` L ) ` x ) ( D Nat C ) ( ( 1st ` L ) ` y ) ) )
70 5 fveq2d 
 |-  ( ph -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) )
71 70 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) )
72 68 69 71 53 prcof21a 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` L ) ` x ) ( 2nd ` G ) ( ( 1st ` L ) ` y ) ) ` ( ( Base ` D ) X. { f } ) ) = ( ( ( Base ` D ) X. { f } ) o. ( 1st ` F ) ) )
73 63 67 72 3eqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( G o.func L ) ) y ) ` f ) = ( ( ( Base ` D ) X. { f } ) o. ( 1st ` F ) ) )
74 19 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> E e. Cat )
75 2 6 51 41 64 74 60 61 62 diag2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` M ) y ) ` f ) = ( ( Base ` E ) X. { f } ) )
76 57 73 75 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( G o.func L ) ) y ) ` f ) = ( ( x ( 2nd ` M ) y ) ` f ) )
77 47 50 76 eqfnfvd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( G o.func L ) ) y ) = ( x ( 2nd ` M ) y ) )
78 39 40 77 eqfnovd 
 |-  ( ph -> ( 2nd ` ( G o.func L ) ) = ( 2nd ` M ) )
79 38 78 opeq12d 
 |-  ( ph -> <. ( 1st ` ( G o.func L ) ) , ( 2nd ` ( G o.func L ) ) >. = <. ( 1st ` M ) , ( 2nd ` M ) >. )
80 relfunc 
 |-  Rel ( C Func ( E FuncCat C ) )
81 1st2nd 
 |-  ( ( Rel ( C Func ( E FuncCat C ) ) /\ ( G o.func L ) e. ( C Func ( E FuncCat C ) ) ) -> ( G o.func L ) = <. ( 1st ` ( G o.func L ) ) , ( 2nd ` ( G o.func L ) ) >. )
82 80 15 81 sylancr 
 |-  ( ph -> ( G o.func L ) = <. ( 1st ` ( G o.func L ) ) , ( 2nd ` ( G o.func L ) ) >. )
83 1st2nd 
 |-  ( ( Rel ( C Func ( E FuncCat C ) ) /\ M e. ( C Func ( E FuncCat C ) ) ) -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
84 80 20 83 sylancr 
 |-  ( ph -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
85 79 82 84 3eqtr4d 
 |-  ( ph -> ( G o.func L ) = M )