Metamath Proof Explorer

Theorem evlfcllem

Description: Lemma for evlfcl . (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses evlfcl.e 
|- E = ( C evalF D )
evlfcl.q 
|- Q = ( C FuncCat D )
evlfcl.c 
|- ( ph -> C e. Cat )
evlfcl.d 
|- ( ph -> D e. Cat )
evlfcl.n 
|- N = ( C Nat D )
evlfcl.f 
|- ( ph -> ( F e. ( C Func D ) /\ X e. ( Base ` C ) ) )
evlfcl.g 
|- ( ph -> ( G e. ( C Func D ) /\ Y e. ( Base ` C ) ) )
evlfcl.h 
|- ( ph -> ( H e. ( C Func D ) /\ Z e. ( Base ` C ) ) )
evlfcl.a 
|- ( ph -> ( A e. ( F N G ) /\ K e. ( X ( Hom ` C ) Y ) ) )
evlfcl.b 
|- ( ph -> ( B e. ( G N H ) /\ L e. ( Y ( Hom ` C ) Z ) ) )
Assertion evlfcllem 
|- ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. ( comp ` ( Q Xc. C ) ) <. H , Z >. ) <. A , K >. ) ) = ( ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. ) ( <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. ( comp ` D ) ( ( 1st ` E ) ` <. H , Z >. ) ) ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. ) ) )

Proof

Step Hyp Ref Expression
1 evlfcl.e 
 |-  E = ( C evalF D )
2 evlfcl.q 
 |-  Q = ( C FuncCat D )
3 evlfcl.c 
 |-  ( ph -> C e. Cat )
4 evlfcl.d 
 |-  ( ph -> D e. Cat )
5 evlfcl.n 
 |-  N = ( C Nat D )
6 evlfcl.f 
 |-  ( ph -> ( F e. ( C Func D ) /\ X e. ( Base ` C ) ) )
7 evlfcl.g 
 |-  ( ph -> ( G e. ( C Func D ) /\ Y e. ( Base ` C ) ) )
8 evlfcl.h 
 |-  ( ph -> ( H e. ( C Func D ) /\ Z e. ( Base ` C ) ) )
9 evlfcl.a 
 |-  ( ph -> ( A e. ( F N G ) /\ K e. ( X ( Hom ` C ) Y ) ) )
10 evlfcl.b 
 |-  ( ph -> ( B e. ( G N H ) /\ L e. ( Y ( Hom ` C ) Z ) ) )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 eqid 
 |-  ( comp ` D ) = ( comp ` D )
14 6 simpld 
 |-  ( ph -> F e. ( C Func D ) )
15 8 simpld 
 |-  ( ph -> H e. ( C Func D ) )
16 6 simprd 
 |-  ( ph -> X e. ( Base ` C ) )
17 8 simprd 
 |-  ( ph -> Z e. ( Base ` C ) )
18 eqid 
 |-  ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) = ( <. F , X >. ( 2nd ` E ) <. H , Z >. )
19 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
20 9 simpld 
 |-  ( ph -> A e. ( F N G ) )
21 10 simpld 
 |-  ( ph -> B e. ( G N H ) )
22 2 5 19 20 21 fuccocl 
 |-  ( ph -> ( B ( <. F , G >. ( comp ` Q ) H ) A ) e. ( F N H ) )
23 eqid 
 |-  ( comp ` C ) = ( comp ` C )
24 7 simprd 
 |-  ( ph -> Y e. ( Base ` C ) )
25 9 simprd 
 |-  ( ph -> K e. ( X ( Hom ` C ) Y ) )
26 10 simprd 
 |-  ( ph -> L e. ( Y ( Hom ` C ) Z ) )
27 11 12 23 3 16 24 17 25 26 catcocl 
 |-  ( ph -> ( L ( <. X , Y >. ( comp ` C ) Z ) K ) e. ( X ( Hom ` C ) Z ) )
28 1 3 4 11 12 13 5 14 15 16 17 18 22 27 evlf2val 
 |-  ( ph -> ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) = ( ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ` Z ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) ) )
29 2 5 11 13 19 20 21 17 fuccoval 
 |-  ( ph -> ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ` Z ) = ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) )
30 29 oveq1d 
 |-  ( ph -> ( ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ` Z ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) ) )
31 relfunc 
 |-  Rel ( C Func D )
32 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
33 31 14 32 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
34 11 12 23 13 33 16 24 17 25 26 funcco 
 |-  ( ph -> ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) = ( ( ( Y ( 2nd ` F ) Z ) ` L ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` F ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
35 34 oveq2d 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( ( Y ( 2nd ` F ) Z ) ` L ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` F ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
36 5 20 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
37 5 36 11 12 13 24 17 26 nati 
 |-  ( ph -> ( ( A ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) = ( ( ( Y ( 2nd ` G ) Z ) ` L ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( A ` Y ) ) )
38 37 oveq2d 
 |-  ( ph -> ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) ) = ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( ( Y ( 2nd ` G ) Z ) ` L ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( A ` Y ) ) ) )
39 eqid 
 |-  ( Base ` D ) = ( Base ` D )
40 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
41 11 39 33 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
42 41 24 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` Y ) e. ( Base ` D ) )
43 41 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` Z ) e. ( Base ` D ) )
44 7 simpld 
 |-  ( ph -> G e. ( C Func D ) )
45 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
46 31 44 45 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
47 11 39 46 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
48 47 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` Z ) e. ( Base ` D ) )
49 11 12 40 33 24 17 funcf2 
 |-  ( ph -> ( Y ( 2nd ` F ) Z ) : ( Y ( Hom ` C ) Z ) --> ( ( ( 1st ` F ) ` Y ) ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
50 49 26 ffvelrnd 
 |-  ( ph -> ( ( Y ( 2nd ` F ) Z ) ` L ) e. ( ( ( 1st ` F ) ` Y ) ( Hom ` D ) ( ( 1st ` F ) ` Z ) ) )
51 5 36 11 40 17 natcl 
 |-  ( ph -> ( A ` Z ) e. ( ( ( 1st ` F ) ` Z ) ( Hom ` D ) ( ( 1st ` G ) ` Z ) ) )
52 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ H e. ( C Func D ) ) -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
53 31 15 52 sylancr 
 |-  ( ph -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
54 11 39 53 funcf1 
 |-  ( ph -> ( 1st ` H ) : ( Base ` C ) --> ( Base ` D ) )
55 54 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` H ) ` Z ) e. ( Base ` D ) )
56 5 21 nat1st2nd 
 |-  ( ph -> B e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
57 5 56 11 40 17 natcl 
 |-  ( ph -> ( B ` Z ) e. ( ( ( 1st ` G ) ` Z ) ( Hom ` D ) ( ( 1st ` H ) ` Z ) ) )
58 39 40 13 4 42 43 48 50 51 55 57 catass 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) = ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) ) )
59 47 24 ffvelrnd 
 |-  ( ph -> ( ( 1st ` G ) ` Y ) e. ( Base ` D ) )
60 5 36 11 40 24 natcl 
 |-  ( ph -> ( A ` Y ) e. ( ( ( 1st ` F ) ` Y ) ( Hom ` D ) ( ( 1st ` G ) ` Y ) ) )
61 11 12 40 46 24 17 funcf2 
 |-  ( ph -> ( Y ( 2nd ` G ) Z ) : ( Y ( Hom ` C ) Z ) --> ( ( ( 1st ` G ) ` Y ) ( Hom ` D ) ( ( 1st ` G ) ` Z ) ) )
62 61 26 ffvelrnd 
 |-  ( ph -> ( ( Y ( 2nd ` G ) Z ) ` L ) e. ( ( ( 1st ` G ) ` Y ) ( Hom ` D ) ( ( 1st ` G ) ` Z ) ) )
63 39 40 13 4 42 59 48 60 62 55 57 catass 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Y ) ) = ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( ( Y ( 2nd ` G ) Z ) ` L ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Z ) ) ( A ` Y ) ) ) )
64 38 58 63 3eqtr4d 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Y ) ) )
65 64 oveq1d 
 |-  ( ph -> ( ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) = ( ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Y ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
66 41 16 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. ( Base ` D ) )
67 11 12 40 33 16 24 funcf2 
 |-  ( ph -> ( X ( 2nd ` F ) Y ) : ( X ( Hom ` C ) Y ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) )
68 67 25 ffvelrnd 
 |-  ( ph -> ( ( X ( 2nd ` F ) Y ) ` K ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) )
69 39 40 13 4 43 48 55 51 57 catcocl 
 |-  ( ph -> ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) e. ( ( ( 1st ` F ) ` Z ) ( Hom ` D ) ( ( 1st ` H ) ` Z ) ) )
70 39 40 13 4 66 42 43 68 50 55 69 catass 
 |-  ( ph -> ( ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` F ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( ( Y ( 2nd ` F ) Z ) ` L ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` F ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
71 39 40 13 4 59 48 55 62 57 catcocl 
 |-  ( ph -> ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) e. ( ( ( 1st ` G ) ` Y ) ( Hom ` D ) ( ( 1st ` H ) ` Z ) ) )
72 39 40 13 4 66 42 59 68 60 55 71 catass 
 |-  ( ph -> ( ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` Y ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Y ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
73 65 70 72 3eqtr3d 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( ( Y ( 2nd ` F ) Z ) ` L ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` F ) ` Z ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
74 35 73 eqtrd 
 |-  ( ph -> ( ( ( B ` Z ) ( <. ( ( 1st ` F ) ` Z ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( A ` Z ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( X ( 2nd ` F ) Z ) ` ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
75 28 30 74 3eqtrd 
 |-  ( ph -> ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
76 eqid 
 |-  ( Q Xc. C ) = ( Q Xc. C )
77 2 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
78 2 5 fuchom 
 |-  N = ( Hom ` Q )
79 eqid 
 |-  ( comp ` ( Q Xc. C ) ) = ( comp ` ( Q Xc. C ) )
80 76 77 11 78 12 14 16 44 24 19 23 79 15 17 20 25 21 26 xpcco2 
 |-  ( ph -> ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. ( comp ` ( Q Xc. C ) ) <. H , Z >. ) <. A , K >. ) = <. ( B ( <. F , G >. ( comp ` Q ) H ) A ) , ( L ( <. X , Y >. ( comp ` C ) Z ) K ) >. )
81 80 fveq2d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. ( comp ` ( Q Xc. C ) ) <. H , Z >. ) <. A , K >. ) ) = ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` <. ( B ( <. F , G >. ( comp ` Q ) H ) A ) , ( L ( <. X , Y >. ( comp ` C ) Z ) K ) >. ) )
82 df-ov 
 |-  ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) = ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` <. ( B ( <. F , G >. ( comp ` Q ) H ) A ) , ( L ( <. X , Y >. ( comp ` C ) Z ) K ) >. )
83 81 82 eqtr4di 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. ( comp ` ( Q Xc. C ) ) <. H , Z >. ) <. A , K >. ) ) = ( ( B ( <. F , G >. ( comp ` Q ) H ) A ) ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ( L ( <. X , Y >. ( comp ` C ) Z ) K ) ) )
84 df-ov 
 |-  ( F ( 1st ` E ) X ) = ( ( 1st ` E ) ` <. F , X >. )
85 1 3 4 11 14 16 evlf1 
 |-  ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )
86 84 85 eqtr3id 
 |-  ( ph -> ( ( 1st ` E ) ` <. F , X >. ) = ( ( 1st ` F ) ` X ) )
87 df-ov 
 |-  ( G ( 1st ` E ) Y ) = ( ( 1st ` E ) ` <. G , Y >. )
88 1 3 4 11 44 24 evlf1 
 |-  ( ph -> ( G ( 1st ` E ) Y ) = ( ( 1st ` G ) ` Y ) )
89 87 88 eqtr3id 
 |-  ( ph -> ( ( 1st ` E ) ` <. G , Y >. ) = ( ( 1st ` G ) ` Y ) )
90 86 89 opeq12d 
 |-  ( ph -> <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. )
91 df-ov 
 |-  ( H ( 1st ` E ) Z ) = ( ( 1st ` E ) ` <. H , Z >. )
92 1 3 4 11 15 17 evlf1 
 |-  ( ph -> ( H ( 1st ` E ) Z ) = ( ( 1st ` H ) ` Z ) )
93 91 92 eqtr3id 
 |-  ( ph -> ( ( 1st ` E ) ` <. H , Z >. ) = ( ( 1st ` H ) ` Z ) )
94 90 93 oveq12d 
 |-  ( ph -> ( <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. ( comp ` D ) ( ( 1st ` E ) ` <. H , Z >. ) ) = ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) )
95 df-ov 
 |-  ( B ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) L ) = ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. )
96 eqid 
 |-  ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) = ( <. G , Y >. ( 2nd ` E ) <. H , Z >. )
97 1 3 4 11 12 13 5 44 15 24 17 96 21 26 evlf2val 
 |-  ( ph -> ( B ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) L ) = ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) )
98 95 97 eqtr3id 
 |-  ( ph -> ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. ) = ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) )
99 df-ov 
 |-  ( A ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) K ) = ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. )
100 eqid 
 |-  ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) = ( <. F , X >. ( 2nd ` E ) <. G , Y >. )
101 1 3 4 11 12 13 5 14 44 16 24 100 20 25 evlf2val 
 |-  ( ph -> ( A ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) K ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
102 99 101 eqtr3id 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
103 94 98 102 oveq123d 
 |-  ( ph -> ( ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. ) ( <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. ( comp ` D ) ( ( 1st ` E ) ` <. H , Z >. ) ) ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. ) ) = ( ( ( B ` Z ) ( <. ( ( 1st ` G ) ` Y ) , ( ( 1st ` G ) ` Z ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( Y ( 2nd ` G ) Z ) ` L ) ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` Y ) >. ( comp ` D ) ( ( 1st ` H ) ` Z ) ) ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. ( comp ` D ) ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) ) )
104 75 83 103 3eqtr4d 
 |-  ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. ( comp ` ( Q Xc. C ) ) <. H , Z >. ) <. A , K >. ) ) = ( ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. ) ( <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. ( comp ` D ) ( ( 1st ` E ) ` <. H , Z >. ) ) ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. ) ) )