Metamath Proof Explorer

Theorem fucocolem1

Description: Lemma for fucoco . Associativity for morphisms in category E . To simply put, ( ( a .x. b ) .x. ( c .x. d ) ) = ( a .x. ( ( b .x. c ) .x. d ) ) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025)

Ref Expression
Hypotheses fucoco.r 
|- ( ph -> R e. ( F ( D Nat E ) K ) )
fucoco.s 
|- ( ph -> S e. ( G ( C Nat D ) L ) )
fucoco.u 
|- ( ph -> U e. ( K ( D Nat E ) M ) )
fucoco.v 
|- ( ph -> V e. ( L ( C Nat D ) N ) )
fucocolem1.x 
|- ( ph -> X e. ( Base ` C ) )
fucocolem1.p 
|- ( ph -> P e. ( D Func E ) )
fucocolem1.q 
|- ( ph -> Q e. ( C Func D ) )
fucocolem1.a 
|- ( ph -> A e. ( ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) )
fucocolem1.b 
|- ( ph -> B e. ( ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) ( Hom ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) )
Assertion fucocolem1 
|- ( ph -> ( ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) A ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) B ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fucoco.r 
 |-  ( ph -> R e. ( F ( D Nat E ) K ) )
2 fucoco.s 
 |-  ( ph -> S e. ( G ( C Nat D ) L ) )
3 fucoco.u 
 |-  ( ph -> U e. ( K ( D Nat E ) M ) )
4 fucoco.v 
 |-  ( ph -> V e. ( L ( C Nat D ) N ) )
5 fucocolem1.x 
 |-  ( ph -> X e. ( Base ` C ) )
6 fucocolem1.p 
 |-  ( ph -> P e. ( D Func E ) )
7 fucocolem1.q 
 |-  ( ph -> Q e. ( C Func D ) )
8 fucocolem1.a 
 |-  ( ph -> A e. ( ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) )
9 fucocolem1.b 
 |-  ( ph -> B e. ( ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) ( Hom ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) )
10 eqid 
 |-  ( Base ` E ) = ( Base ` E )
11 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
12 eqid 
 |-  ( comp ` E ) = ( comp ` E )
13 relfunc 
 |-  Rel ( D Func E )
14 eqid 
 |-  ( D Nat E ) = ( D Nat E )
15 14 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
16 1 15 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
17 16 simpld 
 |-  ( ph -> F e. ( D Func E ) )
18 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
19 13 17 18 sylancr 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
20 19 funcrcl3 
 |-  ( ph -> E e. Cat )
21 eqid 
 |-  ( Base ` D ) = ( Base ` D )
22 21 10 19 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` D ) --> ( Base ` E ) )
23 eqid 
 |-  ( Base ` C ) = ( Base ` C )
24 relfunc 
 |-  Rel ( C Func D )
25 eqid 
 |-  ( C Nat D ) = ( C Nat D )
26 25 natrcl 
 |-  ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
27 2 26 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
28 27 simpld 
 |-  ( ph -> G e. ( C Func D ) )
29 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
30 24 28 29 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
31 23 21 30 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
32 31 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` G ) ` X ) e. ( Base ` D ) )
33 22 32 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) e. ( Base ` E ) )
34 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ P e. ( D Func E ) ) -> ( 1st ` P ) ( D Func E ) ( 2nd ` P ) )
35 13 6 34 sylancr 
 |-  ( ph -> ( 1st ` P ) ( D Func E ) ( 2nd ` P ) )
36 21 10 35 funcf1 
 |-  ( ph -> ( 1st ` P ) : ( Base ` D ) --> ( Base ` E ) )
37 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ Q e. ( C Func D ) ) -> ( 1st ` Q ) ( C Func D ) ( 2nd ` Q ) )
38 24 7 37 sylancr 
 |-  ( ph -> ( 1st ` Q ) ( C Func D ) ( 2nd ` Q ) )
39 23 21 38 funcf1 
 |-  ( ph -> ( 1st ` Q ) : ( Base ` C ) --> ( Base ` D ) )
40 39 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` Q ) ` X ) e. ( Base ` D ) )
41 36 40 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) e. ( Base ` E ) )
42 16 simprd 
 |-  ( ph -> K e. ( D Func E ) )
43 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
44 13 42 43 sylancr 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
45 21 10 44 funcf1 
 |-  ( ph -> ( 1st ` K ) : ( Base ` D ) --> ( Base ` E ) )
46 25 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
47 4 46 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
48 47 simprd 
 |-  ( ph -> N e. ( C Func D ) )
49 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ N e. ( C Func D ) ) -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
50 24 48 49 sylancr 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
51 23 21 50 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
52 51 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` N ) ` X ) e. ( Base ` D ) )
53 45 52 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) e. ( Base ` E ) )
54 27 simprd 
 |-  ( ph -> L e. ( C Func D ) )
55 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ L e. ( C Func D ) ) -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
56 24 54 55 sylancr 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
57 23 21 56 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
58 57 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` L ) ` X ) e. ( Base ` D ) )
59 22 58 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) e. ( Base ` E ) )
60 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
61 21 60 11 19 32 58 funcf2 
 |-  ( ph -> ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) : ( ( ( 1st ` G ) ` X ) ( Hom ` D ) ( ( 1st ` L ) ` X ) ) --> ( ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) ) )
62 25 2 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
63 25 62 23 60 5 natcl 
 |-  ( ph -> ( S ` X ) e. ( ( ( 1st ` G ) ` X ) ( Hom ` D ) ( ( 1st ` L ) ` X ) ) )
64 61 63 ffvelcdmd 
 |-  ( ph -> ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) ) )
65 10 11 12 20 33 59 41 64 9 catcocl 
 |-  ( ph -> ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) ( Hom ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) )
66 14 natrcl 
 |-  ( U e. ( K ( D Nat E ) M ) -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
67 3 66 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
68 67 simprd 
 |-  ( ph -> M e. ( D Func E ) )
69 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ M e. ( D Func E ) ) -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
70 13 68 69 sylancr 
 |-  ( ph -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
71 21 10 70 funcf1 
 |-  ( ph -> ( 1st ` M ) : ( Base ` D ) --> ( Base ` E ) )
72 71 52 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) e. ( Base ` E ) )
73 14 3 nat1st2nd 
 |-  ( ph -> U e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. ( D Nat E ) <. ( 1st ` M ) , ( 2nd ` M ) >. ) )
74 14 73 21 11 52 natcl 
 |-  ( ph -> ( U ` ( ( 1st ` N ) ` X ) ) e. ( ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ( Hom ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) )
75 10 11 12 20 33 41 53 65 8 72 74 catass 
 |-  ( ph -> ( ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) A ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) ) )
76 10 11 12 20 33 59 41 64 9 53 8 catass 
 |-  ( ph -> ( ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) B ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) = ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) )
77 76 oveq2d 
 |-  ( ph -> ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) B ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) ) )
78 75 77 eqtr4d 
 |-  ( ph -> ( ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) A ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( B ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` X ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) ( ( A ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) , ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) B ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ) ( ( ( ( 1st ` G ) ` X ) ( 2nd ` F ) ( ( 1st ` L ) ` X ) ) ` ( S ` X ) ) ) ) )