Metamath Proof Explorer

Definition df-evlf

Description: Define the evaluation functor, which is the extension of the evaluation map f , x |-> ( fx ) of functors, to a functor ( C --> D ) X. C --> D . (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-evlf 
|- evalF = ( c e. Cat , d e. Cat |-> <. ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cevlf 
 |-  evalF
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vd 
 |-  d
4 vf 
 |-  f
5 1 cv 
 |-  c
6 cfunc 
 |-  Func
7 3 cv 
 |-  d
8 5 7 6 co 
 |-  ( c Func d )
9 vx 
 |-  x
10 cbs 
 |-  Base
11 5 10 cfv 
 |-  ( Base ` c )
12 c1st 
 |-  1st
13 4 cv 
 |-  f
14 13 12 cfv 
 |-  ( 1st ` f )
15 9 cv 
 |-  x
16 15 14 cfv 
 |-  ( ( 1st ` f ) ` x )
17 4 9 8 11 16 cmpo 
 |-  ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) )
18 8 11 cxp 
 |-  ( ( c Func d ) X. ( Base ` c ) )
19 vy 
 |-  y
20 15 12 cfv 
 |-  ( 1st ` x )
21 vm 
 |-  m
22 19 cv 
 |-  y
23 22 12 cfv 
 |-  ( 1st ` y )
24 vn 
 |-  n
25 va 
 |-  a
26 21 cv 
 |-  m
27 cnat 
 |-  Nat
28 5 7 27 co 
 |-  ( c Nat d )
29 24 cv 
 |-  n
30 26 29 28 co 
 |-  ( m ( c Nat d ) n )
31 vg 
 |-  g
32 c2nd 
 |-  2nd
33 15 32 cfv 
 |-  ( 2nd ` x )
34 chom 
 |-  Hom
35 5 34 cfv 
 |-  ( Hom ` c )
36 22 32 cfv 
 |-  ( 2nd ` y )
37 33 36 35 co 
 |-  ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) )
38 25 cv 
 |-  a
39 36 38 cfv 
 |-  ( a ` ( 2nd ` y ) )
40 26 12 cfv 
 |-  ( 1st ` m )
41 33 40 cfv 
 |-  ( ( 1st ` m ) ` ( 2nd ` x ) )
42 36 40 cfv 
 |-  ( ( 1st ` m ) ` ( 2nd ` y ) )
43 41 42 cop 
 |-  <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >.
44 cco 
 |-  comp
45 7 44 cfv 
 |-  ( comp ` d )
46 29 12 cfv 
 |-  ( 1st ` n )
47 36 46 cfv 
 |-  ( ( 1st ` n ) ` ( 2nd ` y ) )
48 43 47 45 co 
 |-  ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) )
49 26 32 cfv 
 |-  ( 2nd ` m )
50 33 36 49 co 
 |-  ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) )
51 31 cv 
 |-  g
52 51 50 cfv 
 |-  ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g )
53 39 52 48 co 
 |-  ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) )
54 25 31 30 37 53 cmpo 
 |-  ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) )
55 24 23 54 csb 
 |-  [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) )
56 21 20 55 csb 
 |-  [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) )
57 9 19 18 18 56 cmpo 
 |-  ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) )
58 17 57 cop 
 |-  <. ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >.
59 1 3 2 2 58 cmpo 
 |-  ( c e. Cat , d e. Cat |-> <. ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
60 0 59 wceq 
 |-  evalF = ( c e. Cat , d e. Cat |-> <. ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )