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 0fi ⊢ ∅ ∈ 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