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 = Vtx G
vtxdg0e.i I = iEdg G
Assertion vtxdg0e U V I = VtxDeg G U = 0

Proof

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