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 eqid 
 |-  ( D Nat E ) = ( D Nat E )
14 13 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
15 1 14 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
16 15 simpld 
 |-  ( ph -> F e. ( D Func E ) )
17 16 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
18 17 funcrcl3 
 |-  ( ph -> E e. Cat )
19 eqid 
 |-  ( Base ` D ) = ( Base ` D )
20 19 10 17 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` D ) --> ( Base ` E ) )
21 eqid 
 |-  ( Base ` C ) = ( Base ` C )
22 eqid 
 |-  ( C Nat D ) = ( C Nat D )
23 22 natrcl 
 |-  ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
24 2 23 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
25 24 simpld 
 |-  ( ph -> G e. ( C Func D ) )
26 25 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
27 21 19 26 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
28 27 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` G ) ` X ) e. ( Base ` D ) )
29 20 28 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` ( ( 1st ` G ) ` X ) ) e. ( Base ` E ) )
30 6 func1st2nd 
 |-  ( ph -> ( 1st ` P ) ( D Func E ) ( 2nd ` P ) )
31 19 10 30 funcf1 
 |-  ( ph -> ( 1st ` P ) : ( Base ` D ) --> ( Base ` E ) )
32 7 func1st2nd 
 |-  ( ph -> ( 1st ` Q ) ( C Func D ) ( 2nd ` Q ) )
33 21 19 32 funcf1 
 |-  ( ph -> ( 1st ` Q ) : ( Base ` C ) --> ( Base ` D ) )
34 33 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` Q ) ` X ) e. ( Base ` D ) )
35 31 34 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` P ) ` ( ( 1st ` Q ) ` X ) ) e. ( Base ` E ) )
36 15 simprd 
 |-  ( ph -> K e. ( D Func E ) )
37 36 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
38 19 10 37 funcf1 
 |-  ( ph -> ( 1st ` K ) : ( Base ` D ) --> ( Base ` E ) )
39 22 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
40 4 39 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
41 40 simprd 
 |-  ( ph -> N e. ( C Func D ) )
42 41 func1st2nd 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
43 21 19 42 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
44 43 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` N ) ` X ) e. ( Base ` D ) )
45 38 44 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) e. ( Base ` E ) )
46 24 simprd 
 |-  ( ph -> L e. ( C Func D ) )
47 46 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
48 21 19 47 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
49 48 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` L ) ` X ) e. ( Base ` D ) )
50 20 49 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` ( ( 1st ` L ) ` X ) ) e. ( Base ` E ) )
51 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
52 19 51 11 17 28 49 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 ) ) ) )
53 22 2 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
54 22 53 21 51 5 natcl 
 |-  ( ph -> ( S ` X ) e. ( ( ( 1st ` G ) ` X ) ( Hom ` D ) ( ( 1st ` L ) ` X ) ) )
55 52 54 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 ) ) ) )
56 10 11 12 18 29 50 35 55 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 ) ) ) )
57 13 natrcl 
 |-  ( U e. ( K ( D Nat E ) M ) -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
58 3 57 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
59 58 simprd 
 |-  ( ph -> M e. ( D Func E ) )
60 59 func1st2nd 
 |-  ( ph -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
61 19 10 60 funcf1 
 |-  ( ph -> ( 1st ` M ) : ( Base ` D ) --> ( Base ` E ) )
62 61 44 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) e. ( Base ` E ) )
63 13 3 nat1st2nd 
 |-  ( ph -> U e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. ( D Nat E ) <. ( 1st ` M ) , ( 2nd ` M ) >. ) )
64 13 63 19 11 44 natcl 
 |-  ( ph -> ( U ` ( ( 1st ` N ) ` X ) ) e. ( ( ( 1st ` K ) ` ( ( 1st ` N ) ` X ) ) ( Hom ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` X ) ) ) )
65 10 11 12 18 29 35 45 56 8 62 64 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 ) ) ) ) ) )
66 10 11 12 18 29 50 35 55 9 45 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 ) ) ) ) )
67 66 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 ) ) ) ) ) )
68 65 67 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 ) ) ) ) )