Metamath Proof Explorer


Theorem diag2

Description: Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses diag2.l L=CΔfuncD
diag2.a A=BaseC
diag2.b B=BaseD
diag2.h H=HomC
diag2.c φCCat
diag2.d φDCat
diag2.x φXA
diag2.y φYA
diag2.f φFXHY
Assertion diag2 φX2ndLYF=B×F

Proof

Step Hyp Ref Expression
1 diag2.l L=CΔfuncD
2 diag2.a A=BaseC
3 diag2.b B=BaseD
4 diag2.h H=HomC
5 diag2.c φCCat
6 diag2.d φDCat
7 diag2.x φXA
8 diag2.y φYA
9 diag2.f φFXHY
10 1 5 6 diagval φL=CDcurryFC1stFD
11 10 fveq2d φ2ndL=2ndCDcurryFC1stFD
12 11 oveqd φX2ndLY=X2ndCDcurryFC1stFDY
13 12 fveq1d φX2ndLYF=X2ndCDcurryFC1stFDYF
14 eqid CDcurryFC1stFD=CDcurryFC1stFD
15 eqid C×cD=C×cD
16 eqid C1stFD=C1stFD
17 15 5 6 16 1stfcl φC1stFDC×cDFuncC
18 eqid IdD=IdD
19 eqid X2ndCDcurryFC1stFDYF=X2ndCDcurryFC1stFDYF
20 14 2 5 6 17 3 4 18 7 8 9 19 curf2 φX2ndCDcurryFC1stFDYF=xBFXx2ndC1stFDYxIdDx
21 15 2 3 xpcbas A×B=BaseC×cD
22 eqid HomC×cD=HomC×cD
23 5 adantr φxBCCat
24 6 adantr φxBDCat
25 opelxpi XAxBXxA×B
26 7 25 sylan φxBXxA×B
27 opelxpi YAxBYxA×B
28 8 27 sylan φxBYxA×B
29 15 21 22 23 24 16 26 28 1stf2 φxBXx2ndC1stFDYx=1stXxHomC×cDYx
30 29 oveqd φxBFXx2ndC1stFDYxIdDx=F1stXxHomC×cDYxIdDx
31 df-ov F1stXxHomC×cDYxIdDx=1stXxHomC×cDYxFIdDx
32 9 adantr φxBFXHY
33 eqid HomD=HomD
34 simpr φxBxB
35 3 33 18 24 34 catidcl φxBIdDxxHomDx
36 32 35 opelxpd φxBFIdDxXHY×xHomDx
37 7 adantr φxBXA
38 8 adantr φxBYA
39 15 2 3 4 33 37 34 38 34 22 xpchom2 φxBXxHomC×cDYx=XHY×xHomDx
40 36 39 eleqtrrd φxBFIdDxXxHomC×cDYx
41 40 fvresd φxB1stXxHomC×cDYxFIdDx=1stFIdDx
42 31 41 eqtrid φxBF1stXxHomC×cDYxIdDx=1stFIdDx
43 op1stg FXHYIdDxxHomDx1stFIdDx=F
44 9 35 43 syl2an2r φxB1stFIdDx=F
45 30 42 44 3eqtrd φxBFXx2ndC1stFDYxIdDx=F
46 45 mpteq2dva φxBFXx2ndC1stFDYxIdDx=xBF
47 fconstmpt B×F=xBF
48 46 47 eqtr4di φxBFXx2ndC1stFDYxIdDx=B×F
49 13 20 48 3eqtrd φX2ndLYF=B×F