Metamath Proof Explorer


Theorem natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses natfval.1 N=CNatD
natfval.b B=BaseC
natfval.h H=HomC
natfval.j J=HomD
natfval.o ·˙=compD
Assertion natfval N=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax

Proof

Step Hyp Ref Expression
1 natfval.1 N=CNatD
2 natfval.b B=BaseC
3 natfval.h H=HomC
4 natfval.j J=HomD
5 natfval.o ·˙=compD
6 oveq12 t=Cu=DtFuncu=CFuncD
7 simpl t=Cu=Dt=C
8 7 fveq2d t=Cu=DBaset=BaseC
9 8 2 eqtr4di t=Cu=DBaset=B
10 9 ixpeq1d t=Cu=DxBasetrxHomusx=xBrxHomusx
11 simpr t=Cu=Du=D
12 11 fveq2d t=Cu=DHomu=HomD
13 12 4 eqtr4di t=Cu=DHomu=J
14 13 oveqd t=Cu=DrxHomusx=rxJsx
15 14 ixpeq2dv t=Cu=DxBrxHomusx=xBrxJsx
16 10 15 eqtrd t=Cu=DxBasetrxHomusx=xBrxJsx
17 7 fveq2d t=Cu=DHomt=HomC
18 17 3 eqtr4di t=Cu=DHomt=H
19 18 oveqd t=Cu=DxHomty=xHy
20 11 fveq2d t=Cu=Dcompu=compD
21 20 5 eqtr4di t=Cu=Dcompu=·˙
22 21 oveqd t=Cu=Drxrycompusy=rxry·˙sy
23 22 oveqd t=Cu=Dayrxrycompusyx2ndfyh=ayrxry·˙syx2ndfyh
24 21 oveqd t=Cu=Drxsxcompusy=rxsx·˙sy
25 24 oveqd t=Cu=Dx2ndgyhrxsxcompusyax=x2ndgyhrxsx·˙syax
26 23 25 eqeq12d t=Cu=Dayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyaxayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
27 19 26 raleqbidv t=Cu=DhxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyaxhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
28 9 27 raleqbidv t=Cu=DyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyaxyBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
29 9 28 raleqbidv t=Cu=DxBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyaxxByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
30 16 29 rabeqbidv t=Cu=DaxBasetrxHomusx|xBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyax=axBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
31 30 csbeq2dv t=Cu=D1stg/saxBasetrxHomusx|xBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyax=1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
32 31 csbeq2dv t=Cu=D1stf/r1stg/saxBasetrxHomusx|xBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyax=1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
33 6 6 32 mpoeq123dv t=Cu=DftFuncu,gtFuncu1stf/r1stg/saxBasetrxHomusx|xBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyax=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
34 df-nat Nat=tCat,uCatftFuncu,gtFuncu1stf/r1stg/saxBasetrxHomusx|xBasetyBasethxHomtyayrxrycompusyx2ndfyh=x2ndgyhrxsxcompusyax
35 ovex CFuncDV
36 35 35 mpoex fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syaxV
37 33 34 36 ovmpoa CCatDCatCNatD=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
38 34 mpondm0 ¬CCatDCatCNatD=
39 funcrcl fCFuncDCCatDCat
40 39 con3i ¬CCatDCat¬fCFuncD
41 40 eq0rdv ¬CCatDCatCFuncD=
42 41 olcd ¬CCatDCatCFuncD=CFuncD=
43 0mpo0 CFuncD=CFuncD=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax=
44 42 43 syl ¬CCatDCatfCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax=
45 38 44 eqtr4d ¬CCatDCatCNatD=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
46 37 45 pm2.61i CNatD=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax
47 1 46 eqtri N=fCFuncD,gCFuncD1stf/r1stg/saxBrxJsx|xByBhxHyayrxry·˙syx2ndfyh=x2ndgyhrxsx·˙syax