Metamath Proof Explorer


Theorem vtxdg0e

Description: The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai , vdegp1bi and vdegp1ci ). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxdgf.v V=VtxG
vtxdg0e.i I=iEdgG
Assertion vtxdg0e UVI=VtxDegGU=0

Proof

Step Hyp Ref Expression
1 vtxdgf.v V=VtxG
2 vtxdg0e.i I=iEdgG
3 2 eqeq1i I=iEdgG=
4 dmeq iEdgG=domiEdgG=dom
5 dm0 dom=
6 4 5 eqtrdi iEdgG=domiEdgG=
7 0fin Fin
8 6 7 eqeltrdi iEdgG=domiEdgGFin
9 3 8 sylbi I=domiEdgGFin
10 simpl UVI=UV
11 eqid iEdgG=iEdgG
12 eqid domiEdgG=domiEdgG
13 1 11 12 vtxdgfival domiEdgGFinUVVtxDegGU=xdomiEdgG|UiEdgGx+xdomiEdgG|iEdgGx=U
14 9 10 13 syl2an2 UVI=VtxDegGU=xdomiEdgG|UiEdgGx+xdomiEdgG|iEdgGx=U
15 3 6 sylbi I=domiEdgG=
16 15 adantl UVI=domiEdgG=
17 rabeq domiEdgG=xdomiEdgG|UiEdgGx=x|UiEdgGx
18 rab0 x|UiEdgGx=
19 17 18 eqtrdi domiEdgG=xdomiEdgG|UiEdgGx=
20 19 fveq2d domiEdgG=xdomiEdgG|UiEdgGx=
21 hash0 =0
22 20 21 eqtrdi domiEdgG=xdomiEdgG|UiEdgGx=0
23 rabeq domiEdgG=xdomiEdgG|iEdgGx=U=x|iEdgGx=U
24 23 fveq2d domiEdgG=xdomiEdgG|iEdgGx=U=x|iEdgGx=U
25 rab0 x|iEdgGx=U=
26 25 fveq2i x|iEdgGx=U=
27 26 21 eqtri x|iEdgGx=U=0
28 24 27 eqtrdi domiEdgG=xdomiEdgG|iEdgGx=U=0
29 22 28 oveq12d domiEdgG=xdomiEdgG|UiEdgGx+xdomiEdgG|iEdgGx=U=0+0
30 16 29 syl UVI=xdomiEdgG|UiEdgGx+xdomiEdgG|iEdgGx=U=0+0
31 00id 0+0=0
32 30 31 eqtrdi UVI=xdomiEdgG|UiEdgGx+xdomiEdgG|iEdgGx=U=0
33 14 32 eqtrd UVI=VtxDegGU=0