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 = Vtx (G)$
	vtxdginducedm1.e	$⊢ E = iEdg (G)$
	vtxdginducedm1.k	$⊢ K = V ∖ \{N\}$
	vtxdginducedm1.i	$⊢ I = \{i \in dom E \| N \notin E (i)\}$
	vtxdginducedm1.p	$⊢ P = {E ↾}_{I}$
	vtxdginducedm1.s	$⊢ S = ⟨K, P⟩$
	vtxdginducedm1.j	$⊢ J = \{i \in dom E \| N \in E (i)\}$
Assertion	vtxdginducedm1	$⊢ \forall v \in (V ∖ \{N\}) VtxDeg (G) (v) = VtxDeg (S) (v) +_{𝑒} \|\{l \in J \| v \in E (l)\}\|$

Proof

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

Metamath Proof Explorer

Theorem vtxdginducedm1

Proof