This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )