MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-evlf Unicode version

Definition df-evlf 14003
Description: Define the evaluation functor, which is the extension of the evaluation map  f ,  x  |->  ( f `  x
) of functors, to a functor  ( C --> D )  X.  C --> D. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
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 ) ) ) ) >. )
Distinct variable group:    a, c, d, f, g, m, n, x, y

Detailed syntax breakdown of Definition df-evlf
StepHypRef Expression
1 cevlf 13999 . 2  class evalF
2 vc . . 3  set  c
3 vd . . 3  set  d
4 ccat 13582 . . 3  class  Cat
5 vf . . . . 5  set  f
6 vx . . . . 5  set  x
72cv 1631 . . . . . 6  class  c
83cv 1631 . . . . . 6  class  d
9 cfunc 13744 . . . . . 6  class  Func
107, 8, 9co 5874 . . . . 5  class  ( c 
Func  d )
11 cbs 13164 . . . . . 6  class  Base
127, 11cfv 5271 . . . . 5  class  ( Base `  c )
136cv 1631 . . . . . 6  class  x
145cv 1631 . . . . . . 7  class  f
15 c1st 6136 . . . . . . 7  class  1st
1614, 15cfv 5271 . . . . . 6  class  ( 1st `  f )
1713, 16cfv 5271 . . . . 5  class  ( ( 1st `  f ) `
 x )
185, 6, 10, 12, 17cmpt2 5876 . . . 4  class  ( f  e.  ( c  Func  d ) ,  x  e.  ( Base `  c
)  |->  ( ( 1st `  f ) `  x
) )
19 vy . . . . 5  set  y
2010, 12cxp 4703 . . . . 5  class  ( ( c  Func  d )  X.  ( Base `  c
) )
21 vm . . . . . 6  set  m
2213, 15cfv 5271 . . . . . 6  class  ( 1st `  x )
23 vn . . . . . . 7  set  n
2419cv 1631 . . . . . . . 8  class  y
2524, 15cfv 5271 . . . . . . 7  class  ( 1st `  y )
26 va . . . . . . . 8  set  a
27 vg . . . . . . . 8  set  g
2821cv 1631 . . . . . . . . 9  class  m
2923cv 1631 . . . . . . . . 9  class  n
30 cnat 13831 . . . . . . . . . 10  class Nat
317, 8, 30co 5874 . . . . . . . . 9  class  ( c Nat  d )
3228, 29, 31co 5874 . . . . . . . 8  class  ( m ( c Nat  d ) n )
33 c2nd 6137 . . . . . . . . . 10  class  2nd
3413, 33cfv 5271 . . . . . . . . 9  class  ( 2nd `  x )
3524, 33cfv 5271 . . . . . . . . 9  class  ( 2nd `  y )
36 chom 13235 . . . . . . . . . 10  class  Hom
377, 36cfv 5271 . . . . . . . . 9  class  (  Hom  `  c )
3834, 35, 37co 5874 . . . . . . . 8  class  ( ( 2nd `  x ) (  Hom  `  c
) ( 2nd `  y
) )
3926cv 1631 . . . . . . . . . 10  class  a
4035, 39cfv 5271 . . . . . . . . 9  class  ( a `
 ( 2nd `  y
) )
4127cv 1631 . . . . . . . . . 10  class  g
4228, 33cfv 5271 . . . . . . . . . . 11  class  ( 2nd `  m )
4334, 35, 42co 5874 . . . . . . . . . 10  class  ( ( 2nd `  x ) ( 2nd `  m
) ( 2nd `  y
) )
4441, 43cfv 5271 . . . . . . . . 9  class  ( ( ( 2nd `  x
) ( 2nd `  m
) ( 2nd `  y
) ) `  g
)
4528, 15cfv 5271 . . . . . . . . . . . 12  class  ( 1st `  m )
4634, 45cfv 5271 . . . . . . . . . . 11  class  ( ( 1st `  m ) `
 ( 2nd `  x
) )
4735, 45cfv 5271 . . . . . . . . . . 11  class  ( ( 1st `  m ) `
 ( 2nd `  y
) )
4846, 47cop 3656 . . . . . . . . . 10  class  <. (
( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
4929, 15cfv 5271 . . . . . . . . . . 11  class  ( 1st `  n )
5035, 49cfv 5271 . . . . . . . . . 10  class  ( ( 1st `  n ) `
 ( 2nd `  y
) )
51 cco 13236 . . . . . . . . . . 11  class comp
528, 51cfv 5271 . . . . . . . . . 10  class  (comp `  d )
5348, 50, 52co 5874 . . . . . . . . 9  class  ( <.
( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  d )
( ( 1st `  n
) `  ( 2nd `  y ) ) )
5440, 44, 53co 5874 . . . . . . . 8  class  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  d )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) )
5526, 27, 32, 38, 54cmpt2 5876 . . . . . . 7  class  ( 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 ) ) )
5623, 25, 55csb 3094 . . . . . 6  class  [_ ( 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 ) ) )
5721, 22, 56csb 3094 . . . . 5  class  [_ ( 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 ) ) )
586, 19, 20, 20, 57cmpt2 5876 . . . 4  class  ( 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 ) ) ) )
5918, 58cop 3656 . . 3  class  <. (
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 ) ) ) ) >.
602, 3, 4, 4, 59cmpt2 5876 . 2  class  ( 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 ) ) ) ) >. )
611, 60wceq 1632 1  wff 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 ) ) ) ) >. )
Colors of variables: wff set class
This definition is referenced by:  evlfval  14007
  Copyright terms: Public domain W3C validator