Metamath Proof Explorer

Theorem diag12

Description: Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l 
|- L = ( C DiagFunc D )
diagval.c 
|- ( ph -> C e. Cat )
diagval.d 
|- ( ph -> D e. Cat )
diag11.a 
|- A = ( Base ` C )
diag11.c 
|- ( ph -> X e. A )
diag11.k 
|- K = ( ( 1st ` L ) ` X )
diag11.b 
|- B = ( Base ` D )
diag11.y 
|- ( ph -> Y e. B )
diag12.j 
|- J = ( Hom ` D )
diag12.i 
|- .1. = ( Id ` C )
diag12.z 
|- ( ph -> Z e. B )
diag12.f 
|- ( ph -> F e. ( Y J Z ) )
Assertion diag12 
|- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` F ) = ( .1. ` X ) )

Proof

Step Hyp Ref Expression
1 diagval.l 
 |-  L = ( C DiagFunc D )
2 diagval.c 
 |-  ( ph -> C e. Cat )
3 diagval.d 
 |-  ( ph -> D e. Cat )
4 diag11.a 
 |-  A = ( Base ` C )
5 diag11.c 
 |-  ( ph -> X e. A )
6 diag11.k 
 |-  K = ( ( 1st ` L ) ` X )
7 diag11.b 
 |-  B = ( Base ` D )
8 diag11.y 
 |-  ( ph -> Y e. B )
9 diag12.j 
 |-  J = ( Hom ` D )
10 diag12.i 
 |-  .1. = ( Id ` C )
11 diag12.z 
 |-  ( ph -> Z e. B )
12 diag12.f 
 |-  ( ph -> F e. ( Y J Z ) )
13 1 2 3 diagval 
 |-  ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) )
14 13 fveq2d 
 |-  ( ph -> ( 1st ` L ) = ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( 1st ` L ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) )
16 6 15 eqtrid 
 |-  ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) )
17 16 fveq2d 
 |-  ( ph -> ( 2nd ` K ) = ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) )
18 17 oveqd 
 |-  ( ph -> ( Y ( 2nd ` K ) Z ) = ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) Z ) )
19 18 fveq1d 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` F ) = ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) Z ) ` F ) )
20 eqid 
 |-  ( <. C , D >. curryF ( C 1stF D ) ) = ( <. C , D >. curryF ( C 1stF D ) )
21 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
22 eqid 
 |-  ( C 1stF D ) = ( C 1stF D )
23 21 2 3 22 1stfcl 
 |-  ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) )
24 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X )
25 20 4 2 3 23 7 5 24 8 9 10 11 12 curf12 
 |-  ( ph -> ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( C 1stF D ) ) ) ` X ) ) Z ) ` F ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) F ) )
26 df-ov 
 |-  ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) F ) = ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) ` <. ( .1. ` X ) , F >. )
27 21 4 7 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
28 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
29 5 8 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( A X. B ) )
30 5 11 opelxpd 
 |-  ( ph -> <. X , Z >. e. ( A X. B ) )
31 21 27 28 2 3 22 29 30 1stf2 
 |-  ( ph -> ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) = ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) ) )
32 31 fveq1d 
 |-  ( ph -> ( ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) ` <. ( .1. ` X ) , F >. ) = ( ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) ) ` <. ( .1. ` X ) , F >. ) )
33 26 32 eqtrid 
 |-  ( ph -> ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) F ) = ( ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) ) ` <. ( .1. ` X ) , F >. ) )
34 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
35 4 34 10 2 5 catidcl 
 |-  ( ph -> ( .1. ` X ) e. ( X ( Hom ` C ) X ) )
36 35 12 opelxpd 
 |-  ( ph -> <. ( .1. ` X ) , F >. e. ( ( X ( Hom ` C ) X ) X. ( Y J Z ) ) )
37 21 4 7 34 9 5 8 5 11 28 xpchom2 
 |-  ( ph -> ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) = ( ( X ( Hom ` C ) X ) X. ( Y J Z ) ) )
38 36 37 eleqtrrd 
 |-  ( ph -> <. ( .1. ` X ) , F >. e. ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) )
39 38 fvresd 
 |-  ( ph -> ( ( 1st |` ( <. X , Y >. ( Hom ` ( C Xc. D ) ) <. X , Z >. ) ) ` <. ( .1. ` X ) , F >. ) = ( 1st ` <. ( .1. ` X ) , F >. ) )
40 op1stg 
 |-  ( ( ( .1. ` X ) e. ( X ( Hom ` C ) X ) /\ F e. ( Y J Z ) ) -> ( 1st ` <. ( .1. ` X ) , F >. ) = ( .1. ` X ) )
41 35 12 40 syl2anc 
 |-  ( ph -> ( 1st ` <. ( .1. ` X ) , F >. ) = ( .1. ` X ) )
42 33 39 41 3eqtrd 
 |-  ( ph -> ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( C 1stF D ) ) <. X , Z >. ) F ) = ( .1. ` X ) )
43 19 25 42 3eqtrd 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Z ) ` F ) = ( .1. ` X ) )