Metamath Proof Explorer

Theorem evlf2

Description: Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses evlfval.e 
|- E = ( C evalF D )
evlfval.c 
|- ( ph -> C e. Cat )
evlfval.d 
|- ( ph -> D e. Cat )
evlfval.b 
|- B = ( Base ` C )
evlfval.h 
|- H = ( Hom ` C )
evlfval.o 
|- .x. = ( comp ` D )
evlfval.n 
|- N = ( C Nat D )
evlf2.f 
|- ( ph -> F e. ( C Func D ) )
evlf2.g 
|- ( ph -> G e. ( C Func D ) )
evlf2.x 
|- ( ph -> X e. B )
evlf2.y 
|- ( ph -> Y e. B )
evlf2.l 
|- L = ( <. F , X >. ( 2nd ` E ) <. G , Y >. )
Assertion evlf2 
|- ( ph -> L = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )

Proof

Step Hyp Ref Expression
1 evlfval.e 
 |-  E = ( C evalF D )
2 evlfval.c 
 |-  ( ph -> C e. Cat )
3 evlfval.d 
 |-  ( ph -> D e. Cat )
4 evlfval.b 
 |-  B = ( Base ` C )
5 evlfval.h 
 |-  H = ( Hom ` C )
6 evlfval.o 
 |-  .x. = ( comp ` D )
7 evlfval.n 
 |-  N = ( C Nat D )
8 evlf2.f 
 |-  ( ph -> F e. ( C Func D ) )
9 evlf2.g 
 |-  ( ph -> G e. ( C Func D ) )
10 evlf2.x 
 |-  ( ph -> X e. B )
11 evlf2.y 
 |-  ( ph -> Y e. B )
12 evlf2.l 
 |-  L = ( <. F , X >. ( 2nd ` E ) <. G , Y >. )
13 1 2 3 4 5 6 7 evlfval 
 |-  ( ph -> E = <. ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
14 ovex 
 |-  ( C Func D ) e. _V
15 4 fvexi 
 |-  B e. _V
16 14 15 mpoex 
 |-  ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) e. _V
17 14 15 xpex 
 |-  ( ( C Func D ) X. B ) e. _V
18 17 17 mpoex 
 |-  ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) e. _V
19 16 18 op2ndd 
 |-  ( E = <. ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. -> ( 2nd ` E ) = ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) )
20 13 19 syl 
 |-  ( ph -> ( 2nd ` E ) = ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) )
21 fvexd 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> ( 1st ` x ) e. _V )
22 simprl 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> x = <. F , X >. )
23 22 fveq2d 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> ( 1st ` x ) = ( 1st ` <. F , X >. ) )
24 op1stg 
 |-  ( ( F e. ( C Func D ) /\ X e. B ) -> ( 1st ` <. F , X >. ) = F )
25 8 10 24 syl2anc 
 |-  ( ph -> ( 1st ` <. F , X >. ) = F )
26 25 adantr 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> ( 1st ` <. F , X >. ) = F )
27 23 26 eqtrd 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> ( 1st ` x ) = F )
28 fvexd 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> ( 1st ` y ) e. _V )
29 simplrr 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> y = <. G , Y >. )
30 29 fveq2d 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> ( 1st ` y ) = ( 1st ` <. G , Y >. ) )
31 op1stg 
 |-  ( ( G e. ( C Func D ) /\ Y e. B ) -> ( 1st ` <. G , Y >. ) = G )
32 9 11 31 syl2anc 
 |-  ( ph -> ( 1st ` <. G , Y >. ) = G )
33 32 ad2antrr 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> ( 1st ` <. G , Y >. ) = G )
34 30 33 eqtrd 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> ( 1st ` y ) = G )
35 simplr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> m = F )
36 simpr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> n = G )
37 35 36 oveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( m N n ) = ( F N G ) )
38 22 ad2antrr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> x = <. F , X >. )
39 38 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` x ) = ( 2nd ` <. F , X >. ) )
40 op2ndg 
 |-  ( ( F e. ( C Func D ) /\ X e. B ) -> ( 2nd ` <. F , X >. ) = X )
41 8 10 40 syl2anc 
 |-  ( ph -> ( 2nd ` <. F , X >. ) = X )
42 41 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` <. F , X >. ) = X )
43 39 42 eqtrd 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` x ) = X )
44 29 adantr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> y = <. G , Y >. )
45 44 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` y ) = ( 2nd ` <. G , Y >. ) )
46 op2ndg 
 |-  ( ( G e. ( C Func D ) /\ Y e. B ) -> ( 2nd ` <. G , Y >. ) = Y )
47 9 11 46 syl2anc 
 |-  ( ph -> ( 2nd ` <. G , Y >. ) = Y )
48 47 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` <. G , Y >. ) = Y )
49 45 48 eqtrd 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` y ) = Y )
50 43 49 oveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( 2nd ` x ) H ( 2nd ` y ) ) = ( X H Y ) )
51 35 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 1st ` m ) = ( 1st ` F ) )
52 51 43 fveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( 1st ` m ) ` ( 2nd ` x ) ) = ( ( 1st ` F ) ` X ) )
53 51 49 fveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( 1st ` m ) ` ( 2nd ` y ) ) = ( ( 1st ` F ) ` Y ) )
54 52 53 opeq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. )
55 36 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 1st ` n ) = ( 1st ` G ) )
56 55 49 fveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( 1st ` n ) ` ( 2nd ` y ) ) = ( ( 1st ` G ) ` Y ) )
57 54 56 oveq12d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) = ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) )
58 49 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( a ` ( 2nd ` y ) ) = ( a ` Y ) )
59 35 fveq2d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( 2nd ` m ) = ( 2nd ` F ) )
60 59 43 49 oveq123d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) = ( X ( 2nd ` F ) Y ) )
61 60 fveq1d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) = ( ( X ( 2nd ` F ) Y ) ` g ) )
62 57 58 61 oveq123d 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) = ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) )
63 37 50 62 mpoeq123dv 
 |-  ( ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) /\ n = G ) -> ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )
64 28 34 63 csbied2 
 |-  ( ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) /\ m = F ) -> [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )
65 21 27 64 csbied2 
 |-  ( ( ph /\ ( x = <. F , X >. /\ y = <. G , Y >. ) ) -> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )
66 8 10 opelxpd 
 |-  ( ph -> <. F , X >. e. ( ( C Func D ) X. B ) )
67 9 11 opelxpd 
 |-  ( ph -> <. G , Y >. e. ( ( C Func D ) X. B ) )
68 ovex 
 |-  ( F N G ) e. _V
69 ovex 
 |-  ( X H Y ) e. _V
70 68 69 mpoex 
 |-  ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) e. _V
71 70 a1i 
 |-  ( ph -> ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) e. _V )
72 20 65 66 67 71 ovmpod 
 |-  ( ph -> ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )
73 12 72 eqtrid 
 |-  ( ph -> L = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )