Metamath Proof Explorer


Theorem evlfval

Description: Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses evlfval.e E=CevalFD
evlfval.c φCCat
evlfval.d φDCat
evlfval.b B=BaseC
evlfval.h H=HomC
evlfval.o ·˙=compD
evlfval.n N=CNatD
Assertion evlfval φE=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg

Proof

Step Hyp Ref Expression
1 evlfval.e E=CevalFD
2 evlfval.c φCCat
3 evlfval.d φDCat
4 evlfval.b B=BaseC
5 evlfval.h H=HomC
6 evlfval.o ·˙=compD
7 evlfval.n N=CNatD
8 df-evlf evalF=cCat,dCatfcFuncd,xBasec1stfxxcFuncd×Basec,ycFuncd×Basec1stx/m1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg
9 8 a1i φevalF=cCat,dCatfcFuncd,xBasec1stfxxcFuncd×Basec,ycFuncd×Basec1stx/m1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg
10 simprl φc=Cd=Dc=C
11 simprr φc=Cd=Dd=D
12 10 11 oveq12d φc=Cd=DcFuncd=CFuncD
13 10 fveq2d φc=Cd=DBasec=BaseC
14 13 4 eqtr4di φc=Cd=DBasec=B
15 eqidd φc=Cd=D1stfx=1stfx
16 12 14 15 mpoeq123dv φc=Cd=DfcFuncd,xBasec1stfx=fCFuncD,xB1stfx
17 12 14 xpeq12d φc=Cd=DcFuncd×Basec=CFuncD×B
18 10 11 oveq12d φc=Cd=DcNatd=CNatD
19 18 7 eqtr4di φc=Cd=DcNatd=N
20 19 oveqd φc=Cd=DmcNatdn=mNn
21 10 fveq2d φc=Cd=DHomc=HomC
22 21 5 eqtr4di φc=Cd=DHomc=H
23 22 oveqd φc=Cd=D2ndxHomc2ndy=2ndxH2ndy
24 11 fveq2d φc=Cd=Dcompd=compD
25 24 6 eqtr4di φc=Cd=Dcompd=·˙
26 25 oveqd φc=Cd=D1stm2ndx1stm2ndycompd1stn2ndy=1stm2ndx1stm2ndy·˙1stn2ndy
27 26 oveqd φc=Cd=Da2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=a2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
28 20 23 27 mpoeq123dv φc=Cd=DamcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=amNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
29 28 csbeq2dv φc=Cd=D1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
30 29 csbeq2dv φc=Cd=D1stx/m1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
31 17 17 30 mpoeq123dv φc=Cd=DxcFuncd×Basec,ycFuncd×Basec1stx/m1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=xCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
32 16 31 opeq12d φc=Cd=DfcFuncd,xBasec1stfxxcFuncd×Basec,ycFuncd×Basec1stx/m1sty/namcNatdn,g2ndxHomc2ndya2ndy1stm2ndx1stm2ndycompd1stn2ndy2ndx2ndm2ndyg=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
33 opex fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndygV
34 33 a1i φfCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndygV
35 9 32 2 3 34 ovmpod φCevalFD=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg
36 1 35 eqtrid φE=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namNn,g2ndxH2ndya2ndy1stm2ndx1stm2ndy·˙1stn2ndy2ndx2ndm2ndyg