# Metamath Proof Explorer

## Theorem vtxdginducedm1

Description: The degree of a vertex v in the induced subgraph S of a pseudograph G obtained by removing one vertex N plus the number of edges joining the vertex v and the vertex N is the degree of the vertex v in the pseudograph G . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
vtxdginducedm1.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
vtxdginducedm1.k ${⊢}{K}={V}\setminus \left\{{N}\right\}$
vtxdginducedm1.i ${⊢}{I}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
vtxdginducedm1.p ${⊢}{P}={{E}↾}_{{I}}$
vtxdginducedm1.s ${⊢}{S}=⟨{K},{P}⟩$
vtxdginducedm1.j ${⊢}{J}=\left\{{i}\in \mathrm{dom}{E}|{N}\in {E}\left({i}\right)\right\}$
Assertion vtxdginducedm1 ${⊢}\forall {v}\in \left({V}\setminus \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=\mathrm{VtxDeg}\left({S}\right)\left({v}\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$

### Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 vtxdginducedm1.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 vtxdginducedm1.k ${⊢}{K}={V}\setminus \left\{{N}\right\}$
4 vtxdginducedm1.i ${⊢}{I}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
5 vtxdginducedm1.p ${⊢}{P}={{E}↾}_{{I}}$
6 vtxdginducedm1.s ${⊢}{S}=⟨{K},{P}⟩$
7 vtxdginducedm1.j ${⊢}{J}=\left\{{i}\in \mathrm{dom}{E}|{N}\in {E}\left({i}\right)\right\}$
8 7 4 elnelun ${⊢}{J}\cup {I}=\mathrm{dom}{E}$
9 8 eqcomi ${⊢}\mathrm{dom}{E}={J}\cup {I}$
10 9 rabeqi ${⊢}\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}=\left\{{k}\in \left({J}\cup {I}\right)|{v}\in {E}\left({k}\right)\right\}$
11 rabun2 ${⊢}\left\{{k}\in \left({J}\cup {I}\right)|{v}\in {E}\left({k}\right)\right\}=\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cup \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}$
12 10 11 eqtri ${⊢}\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}=\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cup \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}$
13 12 fveq2i ${⊢}\left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cup \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|$
14 2 fvexi ${⊢}{E}\in \mathrm{V}$
15 14 dmex ${⊢}\mathrm{dom}{E}\in \mathrm{V}$
16 7 15 rab2ex ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}$
17 4 15 rab2ex ${⊢}\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}$
18 ssrab2 ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}$
19 ssrab2 ${⊢}\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {I}$
20 ss2in ${⊢}\left(\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}\wedge \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {I}\right)\to \left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}\cap {I}$
21 18 19 20 mp2an ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}\cap {I}$
22 7 4 elneldisj ${⊢}{J}\cap {I}=\varnothing$
23 22 sseq2i ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}\cap {I}↔\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq \varnothing$
24 ss0 ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq \varnothing \to \left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}=\varnothing$
25 23 24 sylbi ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\subseteq {J}\cap {I}\to \left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}=\varnothing$
26 21 25 ax-mp ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}=\varnothing$
27 hashunx ${⊢}\left(\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}\wedge \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}\wedge \left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cap \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}=\varnothing \right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cup \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|$
28 16 17 26 27 mp3an ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\cup \left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|$
29 13 28 eqtri ${⊢}\left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|$
30 9 rabeqi ${⊢}\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in \left({J}\cup {I}\right)|{E}\left({k}\right)=\left\{{v}\right\}\right\}$
31 rabun2 ${⊢}\left\{{k}\in \left({J}\cup {I}\right)|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cup \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}$
32 30 31 eqtri ${⊢}\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cup \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}$
33 32 fveq2i ${⊢}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cup \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
34 7 15 rab2ex ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}$
35 4 15 rab2ex ${⊢}\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}$
36 ssrab2 ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}$
37 ssrab2 ${⊢}\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {I}$
38 ss2in ${⊢}\left(\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}\wedge \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {I}\right)\to \left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}\cap {I}$
39 36 37 38 mp2an ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}\cap {I}$
40 22 sseq2i ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}\cap {I}↔\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq \varnothing$
41 ss0 ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq \varnothing \to \left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\varnothing$
42 40 41 sylbi ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\subseteq {J}\cap {I}\to \left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\varnothing$
43 39 42 ax-mp ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\varnothing$
44 hashunx ${⊢}\left(\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}\wedge \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}\wedge \left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cap \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}=\varnothing \right)\to \left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cup \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
45 34 35 43 44 mp3an ${⊢}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\cup \left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
46 33 45 eqtri ${⊢}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
47 29 46 oveq12i ${⊢}\left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)$
48 hashxnn0 ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
49 16 48 ax-mp ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
50 49 a1i ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
51 hashxnn0 ${⊢}\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\in \mathrm{V}\to \left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
52 17 51 ax-mp ${⊢}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
53 52 a1i ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}$
54 hashxnn0 ${⊢}\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}\to \left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
55 34 54 ax-mp ${⊢}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
56 55 a1i ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
57 hashxnn0 ${⊢}\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\in \mathrm{V}\to \left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
58 35 57 ax-mp ${⊢}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
59 58 a1i ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
60 50 53 56 59 xnn0add4d ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)$
61 xnn0xaddcl ${⊢}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}\wedge \left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}\right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
62 49 55 61 mp2an ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
63 xnn0xr ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}$
64 62 63 ax-mp ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}$
65 xnn0xaddcl ${⊢}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}\wedge \left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}\right)\to \left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
66 52 58 65 mp2an ${⊢}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}$
67 xnn0xr ${⊢}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℕ}_{0}^{*}\to \left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}$
68 66 67 ax-mp ${⊢}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}$
69 xaddcom ${⊢}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}\wedge \left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\in {ℝ}^{*}\right)\to \left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)$
70 64 68 69 mp2an ${⊢}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)$
71 1 2 3 4 5 6 7 vtxdginducedm1lem4 ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=0$
72 71 oveq2d ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}0$
73 xnn0xr ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℕ}_{0}^{*}\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℝ}^{*}$
74 49 73 ax-mp ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℝ}^{*}$
75 xaddid1 ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|\in {ℝ}^{*}\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}0=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|$
76 74 75 ax-mp ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}0=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|$
77 72 76 syl6eq ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|$
78 fveq2 ${⊢}{k}={l}\to {E}\left({k}\right)={E}\left({l}\right)$
79 78 eleq2d ${⊢}{k}={l}\to \left({v}\in {E}\left({k}\right)↔{v}\in {E}\left({l}\right)\right)$
80 79 cbvrabv ${⊢}\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}=\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}$
81 80 fveq2i ${⊢}\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|=\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
82 77 81 syl6eq ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
83 82 oveq2d ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
84 70 83 syl5eq ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
85 60 84 eqtrd ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left(\left|\left\{{k}\in {J}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|\right){+}_{𝑒}\left(\left|\left\{{k}\in {J}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right)=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
86 47 85 syl5eq ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
87 1 2 3 4 5 6 vtxdginducedm1lem2 ${⊢}\mathrm{dom}\mathrm{iEdg}\left({S}\right)={I}$
88 87 rabeqi ${⊢}\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}=\left\{{k}\in {I}|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}$
89 1 2 3 4 5 6 vtxdginducedm1lem3 ${⊢}{k}\in {I}\to \mathrm{iEdg}\left({S}\right)\left({k}\right)={E}\left({k}\right)$
90 89 eleq2d ${⊢}{k}\in {I}\to \left({v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)↔{v}\in {E}\left({k}\right)\right)$
91 90 rabbiia ${⊢}\left\{{k}\in {I}|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}=\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}$
92 88 91 eqtri ${⊢}\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}=\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}$
93 92 fveq2i ${⊢}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|=\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|$
94 87 rabeqi ${⊢}\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in {I}|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}$
95 89 eqeq1d ${⊢}{k}\in {I}\to \left(\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}↔{E}\left({k}\right)=\left\{{v}\right\}\right)$
96 95 rabbiia ${⊢}\left\{{k}\in {I}|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}$
97 94 96 eqtri ${⊢}\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}=\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}$
98 97 fveq2i ${⊢}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
99 93 98 oveq12i ${⊢}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
100 99 eqcomi ${⊢}\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|$
101 100 oveq1i ${⊢}\left(\left|\left\{{k}\in {I}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in {I}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|=\left(\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
102 86 101 syl6eq ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|=\left(\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
103 eldifi ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to {v}\in {V}$
104 eqid ${⊢}\mathrm{dom}{E}=\mathrm{dom}{E}$
105 1 2 104 vtxdgval ${⊢}{v}\in {V}\to \mathrm{VtxDeg}\left({G}\right)\left({v}\right)=\left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
106 103 105 syl ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \mathrm{VtxDeg}\left({G}\right)\left({v}\right)=\left|\left\{{k}\in \mathrm{dom}{E}|{v}\in {E}\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}{E}|{E}\left({k}\right)=\left\{{v}\right\}\right\}\right|$
107 6 fveq2i ${⊢}\mathrm{Vtx}\left({S}\right)=\mathrm{Vtx}\left(⟨{K},{P}⟩\right)$
108 1 fvexi ${⊢}{V}\in \mathrm{V}$
109 difexg ${⊢}{V}\in \mathrm{V}\to {V}\setminus \left\{{N}\right\}\in \mathrm{V}$
110 3 109 eqeltrid ${⊢}{V}\in \mathrm{V}\to {K}\in \mathrm{V}$
111 108 110 ax-mp ${⊢}{K}\in \mathrm{V}$
112 resexg ${⊢}{E}\in \mathrm{V}\to {{E}↾}_{{I}}\in \mathrm{V}$
113 5 112 eqeltrid ${⊢}{E}\in \mathrm{V}\to {P}\in \mathrm{V}$
114 14 113 ax-mp ${⊢}{P}\in \mathrm{V}$
115 111 114 opvtxfvi ${⊢}\mathrm{Vtx}\left(⟨{K},{P}⟩\right)={K}$
116 107 115 eqtri ${⊢}\mathrm{Vtx}\left({S}\right)={K}$
117 116 eleq2i ${⊢}{v}\in \mathrm{Vtx}\left({S}\right)↔{v}\in {K}$
118 3 eleq2i ${⊢}{v}\in {K}↔{v}\in \left({V}\setminus \left\{{N}\right\}\right)$
119 117 118 sylbbr ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to {v}\in \mathrm{Vtx}\left({S}\right)$
120 eqid ${⊢}\mathrm{Vtx}\left({S}\right)=\mathrm{Vtx}\left({S}\right)$
121 eqid ${⊢}\mathrm{iEdg}\left({S}\right)=\mathrm{iEdg}\left({S}\right)$
122 eqid ${⊢}\mathrm{dom}\mathrm{iEdg}\left({S}\right)=\mathrm{dom}\mathrm{iEdg}\left({S}\right)$
123 120 121 122 vtxdgval ${⊢}{v}\in \mathrm{Vtx}\left({S}\right)\to \mathrm{VtxDeg}\left({S}\right)\left({v}\right)=\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|$
124 119 123 syl ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \mathrm{VtxDeg}\left({S}\right)\left({v}\right)=\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|$
125 124 oveq1d ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \mathrm{VtxDeg}\left({S}\right)\left({v}\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|=\left(\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|{v}\in \mathrm{iEdg}\left({S}\right)\left({k}\right)\right\}\right|{+}_{𝑒}\left|\left\{{k}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)|\mathrm{iEdg}\left({S}\right)\left({k}\right)=\left\{{v}\right\}\right\}\right|\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
126 102 106 125 3eqtr4d ${⊢}{v}\in \left({V}\setminus \left\{{N}\right\}\right)\to \mathrm{VtxDeg}\left({G}\right)\left({v}\right)=\mathrm{VtxDeg}\left({S}\right)\left({v}\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$
127 126 rgen ${⊢}\forall {v}\in \left({V}\setminus \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({G}\right)\left({v}\right)=\mathrm{VtxDeg}\left({S}\right)\left({v}\right){+}_{𝑒}\left|\left\{{l}\in {J}|{v}\in {E}\left({l}\right)\right\}\right|$