Metamath Proof Explorer


Theorem vtxdgfval

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Hypotheses vtxdgfval.v V=VtxG
vtxdgfval.i I=iEdgG
vtxdgfval.a A=domI
Assertion vtxdgfval GWVtxDegG=uVxA|uIx+𝑒xA|Ix=u

Proof

Step Hyp Ref Expression
1 vtxdgfval.v V=VtxG
2 vtxdgfval.i I=iEdgG
3 vtxdgfval.a A=domI
4 df-vtxdg VtxDeg=gVVtxg/viEdgg/euvxdome|uex+𝑒xdome|ex=u
5 fvex VtxgV
6 fvex iEdggV
7 simpl v=Vtxge=iEdggv=Vtxg
8 dmeq e=iEdggdome=domiEdgg
9 fveq1 e=iEdggex=iEdggx
10 9 eleq2d e=iEdgguexuiEdggx
11 8 10 rabeqbidv e=iEdggxdome|uex=xdomiEdgg|uiEdggx
12 11 fveq2d e=iEdggxdome|uex=xdomiEdgg|uiEdggx
13 9 eqeq1d e=iEdggex=uiEdggx=u
14 8 13 rabeqbidv e=iEdggxdome|ex=u=xdomiEdgg|iEdggx=u
15 14 fveq2d e=iEdggxdome|ex=u=xdomiEdgg|iEdggx=u
16 12 15 oveq12d e=iEdggxdome|uex+𝑒xdome|ex=u=xdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u
17 16 adantl v=Vtxge=iEdggxdome|uex+𝑒xdome|ex=u=xdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u
18 7 17 mpteq12dv v=Vtxge=iEdgguvxdome|uex+𝑒xdome|ex=u=uVtxgxdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u
19 5 6 18 csbie2 Vtxg/viEdgg/euvxdome|uex+𝑒xdome|ex=u=uVtxgxdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u
20 fveq2 g=GVtxg=VtxG
21 20 1 eqtr4di g=GVtxg=V
22 fveq2 g=GiEdgg=iEdgG
23 22 dmeqd g=GdomiEdgg=domiEdgG
24 2 dmeqi domI=domiEdgG
25 3 24 eqtri A=domiEdgG
26 23 25 eqtr4di g=GdomiEdgg=A
27 22 2 eqtr4di g=GiEdgg=I
28 27 fveq1d g=GiEdggx=Ix
29 28 eleq2d g=GuiEdggxuIx
30 26 29 rabeqbidv g=GxdomiEdgg|uiEdggx=xA|uIx
31 30 fveq2d g=GxdomiEdgg|uiEdggx=xA|uIx
32 28 eqeq1d g=GiEdggx=uIx=u
33 26 32 rabeqbidv g=GxdomiEdgg|iEdggx=u=xA|Ix=u
34 33 fveq2d g=GxdomiEdgg|iEdggx=u=xA|Ix=u
35 31 34 oveq12d g=GxdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u=xA|uIx+𝑒xA|Ix=u
36 21 35 mpteq12dv g=GuVtxgxdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u=uVxA|uIx+𝑒xA|Ix=u
37 36 adantl GWg=GuVtxgxdomiEdgg|uiEdggx+𝑒xdomiEdgg|iEdggx=u=uVxA|uIx+𝑒xA|Ix=u
38 19 37 eqtrid GWg=GVtxg/viEdgg/euvxdome|uex+𝑒xdome|ex=u=uVxA|uIx+𝑒xA|Ix=u
39 elex GWGV
40 1 fvexi VV
41 mptexg VVuVxA|uIx+𝑒xA|Ix=uV
42 40 41 mp1i GWuVxA|uIx+𝑒xA|Ix=uV
43 4 38 39 42 fvmptd2 GWVtxDegG=uVxA|uIx+𝑒xA|Ix=u