Metamath Proof Explorer

Theorem hofcllem

Description: Lemma for hofcl . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofcl.m 
|- M = ( HomF ` C )
hofcl.o 
|- O = ( oppCat ` C )
hofcl.d 
|- D = ( SetCat ` U )
hofcl.c 
|- ( ph -> C e. Cat )
hofcl.u 
|- ( ph -> U e. V )
hofcl.h 
|- ( ph -> ran ( Homf ` C ) C_ U )
hofcllem.b 
|- B = ( Base ` C )
hofcllem.h 
|- H = ( Hom ` C )
hofcllem.x 
|- ( ph -> X e. B )
hofcllem.y 
|- ( ph -> Y e. B )
hofcllem.z 
|- ( ph -> Z e. B )
hofcllem.w 
|- ( ph -> W e. B )
hofcllem.s 
|- ( ph -> S e. B )
hofcllem.t 
|- ( ph -> T e. B )
hofcllem.m 
|- ( ph -> K e. ( Z H X ) )
hofcllem.n 
|- ( ph -> L e. ( Y H W ) )
hofcllem.p 
|- ( ph -> P e. ( S H Z ) )
hofcllem.q 
|- ( ph -> Q e. ( W H T ) )
Assertion hofcllem 
|- ( ph -> ( ( K ( <. S , Z >. ( comp ` C ) X ) P ) ( <. X , Y >. ( 2nd ` M ) <. S , T >. ) ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ) = ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) )

Proof

Step Hyp Ref Expression
1 hofcl.m 
 |-  M = ( HomF ` C )
2 hofcl.o 
 |-  O = ( oppCat ` C )
3 hofcl.d 
 |-  D = ( SetCat ` U )
4 hofcl.c 
 |-  ( ph -> C e. Cat )
5 hofcl.u 
 |-  ( ph -> U e. V )
6 hofcl.h 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
7 hofcllem.b 
 |-  B = ( Base ` C )
8 hofcllem.h 
 |-  H = ( Hom ` C )
9 hofcllem.x 
 |-  ( ph -> X e. B )
10 hofcllem.y 
 |-  ( ph -> Y e. B )
11 hofcllem.z 
 |-  ( ph -> Z e. B )
12 hofcllem.w 
 |-  ( ph -> W e. B )
13 hofcllem.s 
 |-  ( ph -> S e. B )
14 hofcllem.t 
 |-  ( ph -> T e. B )
15 hofcllem.m 
 |-  ( ph -> K e. ( Z H X ) )
16 hofcllem.n 
 |-  ( ph -> L e. ( Y H W ) )
17 hofcllem.p 
 |-  ( ph -> P e. ( S H Z ) )
18 hofcllem.q 
 |-  ( ph -> Q e. ( W H T ) )
19 eqid 
 |-  ( comp ` C ) = ( comp ` C )
20 4 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> C e. Cat )
21 13 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> S e. B )
22 11 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> Z e. B )
23 9 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> X e. B )
24 17 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> P e. ( S H Z ) )
25 15 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> K e. ( Z H X ) )
26 14 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> T e. B )
27 10 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> Y e. B )
28 simpr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> f e. ( X H Y ) )
29 7 8 19 4 10 12 14 16 18 catcocl 
 |-  ( ph -> ( Q ( <. Y , W >. ( comp ` C ) T ) L ) e. ( Y H T ) )
30 29 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( Q ( <. Y , W >. ( comp ` C ) T ) L ) e. ( Y H T ) )
31 7 8 19 20 23 27 26 28 30 catcocl 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) e. ( X H T ) )
32 7 8 19 20 21 22 23 24 25 26 31 catass 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. Z , X >. ( comp ` C ) T ) K ) ( <. S , Z >. ( comp ` C ) T ) P ) = ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. S , X >. ( comp ` C ) T ) ( K ( <. S , Z >. ( comp ` C ) X ) P ) ) )
33 12 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> W e. B )
34 16 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> L e. ( Y H W ) )
35 18 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> Q e. ( W H T ) )
36 7 8 19 20 23 27 33 28 34 26 35 catass 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) = ( Q ( <. X , W >. ( comp ` C ) T ) ( L ( <. X , Y >. ( comp ` C ) W ) f ) ) )
37 36 oveq1d 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. Z , X >. ( comp ` C ) T ) K ) = ( ( Q ( <. X , W >. ( comp ` C ) T ) ( L ( <. X , Y >. ( comp ` C ) W ) f ) ) ( <. Z , X >. ( comp ` C ) T ) K ) )
38 7 8 19 20 23 27 33 28 34 catcocl 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( L ( <. X , Y >. ( comp ` C ) W ) f ) e. ( X H W ) )
39 7 8 19 20 22 23 33 25 38 26 35 catass 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( Q ( <. X , W >. ( comp ` C ) T ) ( L ( <. X , Y >. ( comp ` C ) W ) f ) ) ( <. Z , X >. ( comp ` C ) T ) K ) = ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) )
40 37 39 eqtrd 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. Z , X >. ( comp ` C ) T ) K ) = ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) )
41 40 oveq1d 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. Z , X >. ( comp ` C ) T ) K ) ( <. S , Z >. ( comp ` C ) T ) P ) = ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) )
42 32 41 eqtr3d 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. S , X >. ( comp ` C ) T ) ( K ( <. S , Z >. ( comp ` C ) X ) P ) ) = ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) )
43 42 mpteq2dva 
 |-  ( ph -> ( f e. ( X H Y ) |-> ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. S , X >. ( comp ` C ) T ) ( K ( <. S , Z >. ( comp ` C ) X ) P ) ) ) = ( f e. ( X H Y ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) ) )
44 7 8 19 4 13 11 9 17 15 catcocl 
 |-  ( ph -> ( K ( <. S , Z >. ( comp ` C ) X ) P ) e. ( S H X ) )
45 1 4 7 8 9 10 13 14 19 44 29 hof2val 
 |-  ( ph -> ( ( K ( <. S , Z >. ( comp ` C ) X ) P ) ( <. X , Y >. ( 2nd ` M ) <. S , T >. ) ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ) = ( f e. ( X H Y ) |-> ( ( ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ( <. X , Y >. ( comp ` C ) T ) f ) ( <. S , X >. ( comp ` C ) T ) ( K ( <. S , Z >. ( comp ` C ) X ) P ) ) ) )
46 1 4 7 8 11 12 13 14 19 17 18 hof2val 
 |-  ( ph -> ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) = ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) )
47 1 4 7 8 9 10 11 12 19 15 16 hof2val 
 |-  ( ph -> ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) = ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) )
48 46 47 oveq12d 
 |-  ( ph -> ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) = ( ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ) )
49 eqid 
 |-  ( comp ` D ) = ( comp ` D )
50 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
51 50 7 8 9 10 homfval 
 |-  ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
52 50 7 homffn 
 |-  ( Homf ` C ) Fn ( B X. B )
53 52 a1i 
 |-  ( ph -> ( Homf ` C ) Fn ( B X. B ) )
54 df-f 
 |-  ( ( Homf ` C ) : ( B X. B ) --> U <-> ( ( Homf ` C ) Fn ( B X. B ) /\ ran ( Homf ` C ) C_ U ) )
55 53 6 54 sylanbrc 
 |-  ( ph -> ( Homf ` C ) : ( B X. B ) --> U )
56 55 9 10 fovrnd 
 |-  ( ph -> ( X ( Homf ` C ) Y ) e. U )
57 51 56 eqeltrrd 
 |-  ( ph -> ( X H Y ) e. U )
58 50 7 8 11 12 homfval 
 |-  ( ph -> ( Z ( Homf ` C ) W ) = ( Z H W ) )
59 55 11 12 fovrnd 
 |-  ( ph -> ( Z ( Homf ` C ) W ) e. U )
60 58 59 eqeltrrd 
 |-  ( ph -> ( Z H W ) e. U )
61 50 7 8 13 14 homfval 
 |-  ( ph -> ( S ( Homf ` C ) T ) = ( S H T ) )
62 55 13 14 fovrnd 
 |-  ( ph -> ( S ( Homf ` C ) T ) e. U )
63 61 62 eqeltrrd 
 |-  ( ph -> ( S H T ) e. U )
64 7 8 19 20 22 23 33 25 38 catcocl 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) e. ( Z H W ) )
65 64 fmpttd 
 |-  ( ph -> ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) : ( X H Y ) --> ( Z H W ) )
66 4 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> C e. Cat )
67 13 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> S e. B )
68 11 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> Z e. B )
69 14 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> T e. B )
70 17 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> P e. ( S H Z ) )
71 12 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> W e. B )
72 simpr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> g e. ( Z H W ) )
73 18 adantr 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> Q e. ( W H T ) )
74 7 8 19 66 68 71 69 72 73 catcocl 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> ( Q ( <. Z , W >. ( comp ` C ) T ) g ) e. ( Z H T ) )
75 7 8 19 66 67 68 69 70 74 catcocl 
 |-  ( ( ph /\ g e. ( Z H W ) ) -> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) e. ( S H T ) )
76 75 fmpttd 
 |-  ( ph -> ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) : ( Z H W ) --> ( S H T ) )
77 3 5 49 57 60 63 65 76 setcco 
 |-  ( ph -> ( ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ) = ( ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) o. ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ) )
78 eqidd 
 |-  ( ph -> ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) = ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) )
79 eqidd 
 |-  ( ph -> ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) = ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) )
80 oveq2 
 |-  ( g = ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) -> ( Q ( <. Z , W >. ( comp ` C ) T ) g ) = ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) )
81 80 oveq1d 
 |-  ( g = ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) -> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) = ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) )
82 64 78 79 81 fmptco 
 |-  ( ph -> ( ( g e. ( Z H W ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) g ) ( <. S , Z >. ( comp ` C ) T ) P ) ) o. ( f e. ( X H Y ) |-> ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ) = ( f e. ( X H Y ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) ) )
83 48 77 82 3eqtrd 
 |-  ( ph -> ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) = ( f e. ( X H Y ) |-> ( ( Q ( <. Z , W >. ( comp ` C ) T ) ( ( L ( <. X , Y >. ( comp ` C ) W ) f ) ( <. Z , X >. ( comp ` C ) W ) K ) ) ( <. S , Z >. ( comp ` C ) T ) P ) ) )
84 43 45 83 3eqtr4d 
 |-  ( ph -> ( ( K ( <. S , Z >. ( comp ` C ) X ) P ) ( <. X , Y >. ( 2nd ` M ) <. S , T >. ) ( Q ( <. Y , W >. ( comp ` C ) T ) L ) ) = ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. ( comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) )