Metamath Proof Explorer


Theorem evlf2val

Description: Value of the evaluation natural transformation at an object. (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 >. )
evlf2val.a
|- ( ph -> A e. ( F N G ) )
evlf2val.k
|- ( ph -> K e. ( X H Y ) )
Assertion evlf2val
|- ( ph -> ( A L K ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )

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 evlf2val.a
 |-  ( ph -> A e. ( F N G ) )
14 evlf2val.k
 |-  ( ph -> K e. ( X H Y ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 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 ) ) ) )
16 simprl
 |-  ( ( ph /\ ( a = A /\ g = K ) ) -> a = A )
17 16 fveq1d
 |-  ( ( ph /\ ( a = A /\ g = K ) ) -> ( a ` Y ) = ( A ` Y ) )
18 simprr
 |-  ( ( ph /\ ( a = A /\ g = K ) ) -> g = K )
19 18 fveq2d
 |-  ( ( ph /\ ( a = A /\ g = K ) ) -> ( ( X ( 2nd ` F ) Y ) ` g ) = ( ( X ( 2nd ` F ) Y ) ` K ) )
20 17 19 oveq12d
 |-  ( ( ph /\ ( a = A /\ g = K ) ) -> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
21 ovexd
 |-  ( ph -> ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) e. _V )
22 15 20 13 14 21 ovmpod
 |-  ( ph -> ( A L K ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )