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 | |
|
vtxdg0e.i | |
||
Assertion | vtxdg0e | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxdgf.v | |
|
2 | vtxdg0e.i | |
|
3 | 2 | eqeq1i | |
4 | dmeq | |
|
5 | dm0 | |
|
6 | 4 5 | eqtrdi | |
7 | 0fin | |
|
8 | 6 7 | eqeltrdi | |
9 | 3 8 | sylbi | |
10 | simpl | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 1 11 12 | vtxdgfival | |
14 | 9 10 13 | syl2an2 | |
15 | 3 6 | sylbi | |
16 | 15 | adantl | |
17 | rabeq | |
|
18 | rab0 | |
|
19 | 17 18 | eqtrdi | |
20 | 19 | fveq2d | |
21 | hash0 | |
|
22 | 20 21 | eqtrdi | |
23 | rabeq | |
|
24 | 23 | fveq2d | |
25 | rab0 | |
|
26 | 25 | fveq2i | |
27 | 26 21 | eqtri | |
28 | 24 27 | eqtrdi | |
29 | 22 28 | oveq12d | |
30 | 16 29 | syl | |
31 | 00id | |
|
32 | 30 31 | eqtrdi | |
33 | 14 32 | eqtrd | |