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ΔfuncD
diagval.c φCCat
diagval.d φDCat
diag11.a A=BaseC
diag11.c φXA
diag11.k K=1stLX
diag11.b B=BaseD
diag11.y φYB
diag12.j J=HomD
diag12.i 1˙=IdC
diag12.z φZB
diag12.f φFYJZ
Assertion diag12 φY2ndKZF=1˙X

Proof

Step Hyp Ref Expression
1 diagval.l L=CΔfuncD
2 diagval.c φCCat
3 diagval.d φDCat
4 diag11.a A=BaseC
5 diag11.c φXA
6 diag11.k K=1stLX
7 diag11.b B=BaseD
8 diag11.y φYB
9 diag12.j J=HomD
10 diag12.i 1˙=IdC
11 diag12.z φZB
12 diag12.f φFYJZ
13 1 2 3 diagval φL=CDcurryFC1stFD
14 13 fveq2d φ1stL=1stCDcurryFC1stFD
15 14 fveq1d φ1stLX=1stCDcurryFC1stFDX
16 6 15 eqtrid φK=1stCDcurryFC1stFDX
17 16 fveq2d φ2ndK=2nd1stCDcurryFC1stFDX
18 17 oveqd φY2ndKZ=Y2nd1stCDcurryFC1stFDXZ
19 18 fveq1d φY2ndKZF=Y2nd1stCDcurryFC1stFDXZF
20 eqid CDcurryFC1stFD=CDcurryFC1stFD
21 eqid C×cD=C×cD
22 eqid C1stFD=C1stFD
23 21 2 3 22 1stfcl φC1stFDC×cDFuncC
24 eqid 1stCDcurryFC1stFDX=1stCDcurryFC1stFDX
25 20 4 2 3 23 7 5 24 8 9 10 11 12 curf12 φY2nd1stCDcurryFC1stFDXZF=1˙XXY2ndC1stFDXZF
26 df-ov 1˙XXY2ndC1stFDXZF=XY2ndC1stFDXZ1˙XF
27 21 4 7 xpcbas A×B=BaseC×cD
28 eqid HomC×cD=HomC×cD
29 5 8 opelxpd φXYA×B
30 5 11 opelxpd φXZA×B
31 21 27 28 2 3 22 29 30 1stf2 φXY2ndC1stFDXZ=1stXYHomC×cDXZ
32 31 fveq1d φXY2ndC1stFDXZ1˙XF=1stXYHomC×cDXZ1˙XF
33 26 32 eqtrid φ1˙XXY2ndC1stFDXZF=1stXYHomC×cDXZ1˙XF
34 eqid HomC=HomC
35 4 34 10 2 5 catidcl φ1˙XXHomCX
36 35 12 opelxpd φ1˙XFXHomCX×YJZ
37 21 4 7 34 9 5 8 5 11 28 xpchom2 φXYHomC×cDXZ=XHomCX×YJZ
38 36 37 eleqtrrd φ1˙XFXYHomC×cDXZ
39 38 fvresd φ1stXYHomC×cDXZ1˙XF=1st1˙XF
40 op1stg 1˙XXHomCXFYJZ1st1˙XF=1˙X
41 35 12 40 syl2anc φ1st1˙XF=1˙X
42 33 39 41 3eqtrd φ1˙XXY2ndC1stFDXZF=1˙X
43 19 25 42 3eqtrd φY2ndKZF=1˙X