vtxdun

Description: The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 19-Feb-2021)

	Ref	Expression
Hypotheses	vtxdun.i	$⊢ I = iEdg (G)$
	vtxdun.j	$⊢ J = iEdg (H)$
	vtxdun.vg	$⊢ V = Vtx (G)$
	vtxdun.vh	$⊢ φ \to Vtx (H) = V$
	vtxdun.vu	$⊢ φ \to Vtx (U) = V$
	vtxdun.d	$⊢ φ \to dom I \cap dom J = \emptyset$
	vtxdun.fi	$⊢ φ \to Fun I$
	vtxdun.fj	$⊢ φ \to Fun J$
	vtxdun.n	$⊢ φ \to N \in V$
	vtxdun.u	$⊢ φ \to iEdg (U) = I \cup J$
Assertion	vtxdun	$⊢ φ \to VtxDeg (U) (N) = VtxDeg (G) (N) +_{𝑒} VtxDeg (H) (N)$

Proof

Step	Hyp	Ref	Expression
1		vtxdun.i	$⊢ I = iEdg (G)$
2		vtxdun.j	$⊢ J = iEdg (H)$
3		vtxdun.vg	$⊢ V = Vtx (G)$
4		vtxdun.vh	$⊢ φ \to Vtx (H) = V$
5		vtxdun.vu	$⊢ φ \to Vtx (U) = V$
6		vtxdun.d	$⊢ φ \to dom I \cap dom J = \emptyset$
7		vtxdun.fi	$⊢ φ \to Fun I$
8		vtxdun.fj	$⊢ φ \to Fun J$
9		vtxdun.n	$⊢ φ \to N \in V$
10		vtxdun.u	$⊢ φ \to iEdg (U) = I \cup J$
11		df-rab	$⊢ \{x \in dom iEdg (U) \| N \in iEdg (U) (x)\} = \{x \| (x \in dom iEdg (U) \land N \in iEdg (U) (x))\}$
12	10	dmeqd	$⊢ φ \to dom iEdg (U) = dom (I \cup J)$
13		dmun	$⊢ dom (I \cup J) = dom I \cup dom J$
14	12 13	eqtrdi	$⊢ φ \to dom iEdg (U) = dom I \cup dom J$
15	14	eleq2d	$⊢ φ \to (x \in dom iEdg (U) \leftrightarrow x \in (dom I \cup dom J))$
16		elun	$⊢ x \in (dom I \cup dom J) \leftrightarrow (x \in dom I \lor x \in dom J)$
17	15 16	bitrdi	$⊢ φ \to (x \in dom iEdg (U) \leftrightarrow (x \in dom I \lor x \in dom J))$
18	17	anbi1d	$⊢ φ \to ((x \in dom iEdg (U) \land N \in iEdg (U) (x)) \leftrightarrow ((x \in dom I \lor x \in dom J) \land N \in iEdg (U) (x)))$
19		andir	$⊢ ((x \in dom I \lor x \in dom J) \land N \in iEdg (U) (x)) \leftrightarrow ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))$
20	18 19	bitrdi	$⊢ φ \to ((x \in dom iEdg (U) \land N \in iEdg (U) (x)) \leftrightarrow ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x))))$
21	20	abbidv	$⊢ φ \to \{x \| (x \in dom iEdg (U) \land N \in iEdg (U) (x))\} = \{x \| ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))\}$
22	11 21	syl5eq	$⊢ φ \to \{x \in dom iEdg (U) \| N \in iEdg (U) (x)\} = \{x \| ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))\}$
23		unab	$⊢ \{x \| (x \in dom I \land N \in iEdg (U) (x))\} \cup \{x \| (x \in dom J \land N \in iEdg (U) (x))\} = \{x \| ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))\}$
24	23	eqcomi	$⊢ \{x \| ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))\} = \{x \| (x \in dom I \land N \in iEdg (U) (x))\} \cup \{x \| (x \in dom J \land N \in iEdg (U) (x))\}$
25	24	a1i	$⊢ φ \to \{x \| ((x \in dom I \land N \in iEdg (U) (x)) \lor (x \in dom J \land N \in iEdg (U) (x)))\} = \{x \| (x \in dom I \land N \in iEdg (U) (x))\} \cup \{x \| (x \in dom J \land N \in iEdg (U) (x))\}$
26		df-rab	$⊢ \{x \in dom I \| N \in iEdg (U) (x)\} = \{x \| (x \in dom I \land N \in iEdg (U) (x))\}$
27	10	fveq1d	$⊢ φ \to iEdg (U) (x) = (I \cup J) (x)$
28	27	adantr	$⊢ (φ \land x \in dom I) \to iEdg (U) (x) = (I \cup J) (x)$
29	7	funfnd	$⊢ φ \to I Fn dom I$
30	29	adantr	$⊢ (φ \land x \in dom I) \to I Fn dom I$
31	8	funfnd	$⊢ φ \to J Fn dom J$
32	31	adantr	$⊢ (φ \land x \in dom I) \to J Fn dom J$
33	6	anim1i	$⊢ (φ \land x \in dom I) \to (dom I \cap dom J = \emptyset \land x \in dom I)$
34		fvun1	$⊢ (I Fn dom I \land J Fn dom J \land (dom I \cap dom J = \emptyset \land x \in dom I)) \to (I \cup J) (x) = I (x)$
35	30 32 33 34	syl3anc	$⊢ (φ \land x \in dom I) \to (I \cup J) (x) = I (x)$
36	28 35	eqtrd	$⊢ (φ \land x \in dom I) \to iEdg (U) (x) = I (x)$
37	36	eleq2d	$⊢ (φ \land x \in dom I) \to (N \in iEdg (U) (x) \leftrightarrow N \in I (x))$
38	37	rabbidva	$⊢ φ \to \{x \in dom I \| N \in iEdg (U) (x)\} = \{x \in dom I \| N \in I (x)\}$
39	26 38	eqtr3id	$⊢ φ \to \{x \| (x \in dom I \land N \in iEdg (U) (x))\} = \{x \in dom I \| N \in I (x)\}$
40		df-rab	$⊢ \{x \in dom J \| N \in iEdg (U) (x)\} = \{x \| (x \in dom J \land N \in iEdg (U) (x))\}$
41	27	adantr	$⊢ (φ \land x \in dom J) \to iEdg (U) (x) = (I \cup J) (x)$
42	29	adantr	$⊢ (φ \land x \in dom J) \to I Fn dom I$
43	31	adantr	$⊢ (φ \land x \in dom J) \to J Fn dom J$
44	6	anim1i	$⊢ (φ \land x \in dom J) \to (dom I \cap dom J = \emptyset \land x \in dom J)$
45		fvun2	$⊢ (I Fn dom I \land J Fn dom J \land (dom I \cap dom J = \emptyset \land x \in dom J)) \to (I \cup J) (x) = J (x)$
46	42 43 44 45	syl3anc	$⊢ (φ \land x \in dom J) \to (I \cup J) (x) = J (x)$
47	41 46	eqtrd	$⊢ (φ \land x \in dom J) \to iEdg (U) (x) = J (x)$
48	47	eleq2d	$⊢ (φ \land x \in dom J) \to (N \in iEdg (U) (x) \leftrightarrow N \in J (x))$
49	48	rabbidva	$⊢ φ \to \{x \in dom J \| N \in iEdg (U) (x)\} = \{x \in dom J \| N \in J (x)\}$
50	40 49	eqtr3id	$⊢ φ \to \{x \| (x \in dom J \land N \in iEdg (U) (x))\} = \{x \in dom J \| N \in J (x)\}$
51	39 50	uneq12d	$⊢ φ \to \{x \| (x \in dom I \land N \in iEdg (U) (x))\} \cup \{x \| (x \in dom J \land N \in iEdg (U) (x))\} = \{x \in dom I \| N \in I (x)\} \cup \{x \in dom J \| N \in J (x)\}$
52	22 25 51	3eqtrd	$⊢ φ \to \{x \in dom iEdg (U) \| N \in iEdg (U) (x)\} = \{x \in dom I \| N \in I (x)\} \cup \{x \in dom J \| N \in J (x)\}$
53	52	fveq2d	$⊢ φ \to \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| = \|\{x \in dom I \| N \in I (x)\} \cup \{x \in dom J \| N \in J (x)\}\|$
54	1	fvexi	$⊢ I \in V$
55	54	dmex	$⊢ dom I \in V$
56	55	rabex	$⊢ \{x \in dom I \| N \in I (x)\} \in V$
57	56	a1i	$⊢ φ \to \{x \in dom I \| N \in I (x)\} \in V$
58	2	fvexi	$⊢ J \in V$
59	58	dmex	$⊢ dom J \in V$
60	59	rabex	$⊢ \{x \in dom J \| N \in J (x)\} \in V$
61	60	a1i	$⊢ φ \to \{x \in dom J \| N \in J (x)\} \in V$
62		ssrab2	$⊢ \{x \in dom I \| N \in I (x)\} \subseteq dom I$
63		ssrab2	$⊢ \{x \in dom J \| N \in J (x)\} \subseteq dom J$
64		ss2in	$⊢ (\{x \in dom I \| N \in I (x)\} \subseteq dom I \land \{x \in dom J \| N \in J (x)\} \subseteq dom J) \to \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} \subseteq dom I \cap dom J$
65	62 63 64	mp2an	$⊢ \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} \subseteq dom I \cap dom J$
66	65 6	sseqtrid	$⊢ φ \to \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} \subseteq \emptyset$
67		ss0	$⊢ \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} \subseteq \emptyset \to \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} = \emptyset$
68	66 67	syl	$⊢ φ \to \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} = \emptyset$
69		hashunx	$⊢ (\{x \in dom I \| N \in I (x)\} \in V \land \{x \in dom J \| N \in J (x)\} \in V \land \{x \in dom I \| N \in I (x)\} \cap \{x \in dom J \| N \in J (x)\} = \emptyset) \to \|\{x \in dom I \| N \in I (x)\} \cup \{x \in dom J \| N \in J (x)\}\| = \|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom J \| N \in J (x)\}\|$
70	57 61 68 69	syl3anc	$⊢ φ \to \|\{x \in dom I \| N \in I (x)\} \cup \{x \in dom J \| N \in J (x)\}\| = \|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom J \| N \in J (x)\}\|$
71	53 70	eqtrd	$⊢ φ \to \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| = \|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom J \| N \in J (x)\}\|$
72		df-rab	$⊢ \{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\} = \{x \| (x \in dom iEdg (U) \land iEdg (U) (x) = \{N\})\}$
73	17	anbi1d	$⊢ φ \to ((x \in dom iEdg (U) \land iEdg (U) (x) = \{N\}) \leftrightarrow ((x \in dom I \lor x \in dom J) \land iEdg (U) (x) = \{N\}))$
74		andir	$⊢ ((x \in dom I \lor x \in dom J) \land iEdg (U) (x) = \{N\}) \leftrightarrow ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))$
75	73 74	bitrdi	$⊢ φ \to ((x \in dom iEdg (U) \land iEdg (U) (x) = \{N\}) \leftrightarrow ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\})))$
76	75	abbidv	$⊢ φ \to \{x \| (x \in dom iEdg (U) \land iEdg (U) (x) = \{N\})\} = \{x \| ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))\}$
77	72 76	syl5eq	$⊢ φ \to \{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\} = \{x \| ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))\}$
78		unab	$⊢ \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\} \cup \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\} = \{x \| ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))\}$
79	78	eqcomi	$⊢ \{x \| ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))\} = \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\} \cup \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\}$
80	79	a1i	$⊢ φ \to \{x \| ((x \in dom I \land iEdg (U) (x) = \{N\}) \lor (x \in dom J \land iEdg (U) (x) = \{N\}))\} = \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\} \cup \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\}$
81		df-rab	$⊢ \{x \in dom I \| iEdg (U) (x) = \{N\}\} = \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\}$
82	36	eqeq1d	$⊢ (φ \land x \in dom I) \to (iEdg (U) (x) = \{N\} \leftrightarrow I (x) = \{N\})$
83	82	rabbidva	$⊢ φ \to \{x \in dom I \| iEdg (U) (x) = \{N\}\} = \{x \in dom I \| I (x) = \{N\}\}$
84	81 83	eqtr3id	$⊢ φ \to \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\} = \{x \in dom I \| I (x) = \{N\}\}$
85		df-rab	$⊢ \{x \in dom J \| iEdg (U) (x) = \{N\}\} = \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\}$
86	47	eqeq1d	$⊢ (φ \land x \in dom J) \to (iEdg (U) (x) = \{N\} \leftrightarrow J (x) = \{N\})$
87	86	rabbidva	$⊢ φ \to \{x \in dom J \| iEdg (U) (x) = \{N\}\} = \{x \in dom J \| J (x) = \{N\}\}$
88	85 87	eqtr3id	$⊢ φ \to \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\} = \{x \in dom J \| J (x) = \{N\}\}$
89	84 88	uneq12d	$⊢ φ \to \{x \| (x \in dom I \land iEdg (U) (x) = \{N\})\} \cup \{x \| (x \in dom J \land iEdg (U) (x) = \{N\})\} = \{x \in dom I \| I (x) = \{N\}\} \cup \{x \in dom J \| J (x) = \{N\}\}$
90	77 80 89	3eqtrd	$⊢ φ \to \{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\} = \{x \in dom I \| I (x) = \{N\}\} \cup \{x \in dom J \| J (x) = \{N\}\}$
91	90	fveq2d	$⊢ φ \to \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\| = \|\{x \in dom I \| I (x) = \{N\}\} \cup \{x \in dom J \| J (x) = \{N\}\}\|$
92	55	rabex	$⊢ \{x \in dom I \| I (x) = \{N\}\} \in V$
93	92	a1i	$⊢ φ \to \{x \in dom I \| I (x) = \{N\}\} \in V$
94	59	rabex	$⊢ \{x \in dom J \| J (x) = \{N\}\} \in V$
95	94	a1i	$⊢ φ \to \{x \in dom J \| J (x) = \{N\}\} \in V$
96		ssrab2	$⊢ \{x \in dom I \| I (x) = \{N\}\} \subseteq dom I$
97		ssrab2	$⊢ \{x \in dom J \| J (x) = \{N\}\} \subseteq dom J$
98		ss2in	$⊢ (\{x \in dom I \| I (x) = \{N\}\} \subseteq dom I \land \{x \in dom J \| J (x) = \{N\}\} \subseteq dom J) \to \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} \subseteq dom I \cap dom J$
99	96 97 98	mp2an	$⊢ \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} \subseteq dom I \cap dom J$
100	99 6	sseqtrid	$⊢ φ \to \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} \subseteq \emptyset$
101		ss0	$⊢ \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} \subseteq \emptyset \to \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} = \emptyset$
102	100 101	syl	$⊢ φ \to \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} = \emptyset$
103		hashunx	$⊢ (\{x \in dom I \| I (x) = \{N\}\} \in V \land \{x \in dom J \| J (x) = \{N\}\} \in V \land \{x \in dom I \| I (x) = \{N\}\} \cap \{x \in dom J \| J (x) = \{N\}\} = \emptyset) \to \|\{x \in dom I \| I (x) = \{N\}\} \cup \{x \in dom J \| J (x) = \{N\}\}\| = \|\{x \in dom I \| I (x) = \{N\}\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|$
104	93 95 102 103	syl3anc	$⊢ φ \to \|\{x \in dom I \| I (x) = \{N\}\} \cup \{x \in dom J \| J (x) = \{N\}\}\| = \|\{x \in dom I \| I (x) = \{N\}\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|$
105	91 104	eqtrd	$⊢ φ \to \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\| = \|\{x \in dom I \| I (x) = \{N\}\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|$
106	71 105	oveq12d	$⊢ φ \to \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\| = (\|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom J \| N \in J (x)\}\|) +_{𝑒} (\|\{x \in dom I \| I (x) = \{N\}\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|)$
107		hashxnn0	$⊢ \{x \in dom I \| N \in I (x)\} \in V \to \|\{x \in dom I \| N \in I (x)\}\| \in ℕ_{0}^{*}$
108	57 107	syl	$⊢ φ \to \|\{x \in dom I \| N \in I (x)\}\| \in ℕ_{0}^{*}$
109		hashxnn0	$⊢ \{x \in dom J \| N \in J (x)\} \in V \to \|\{x \in dom J \| N \in J (x)\}\| \in ℕ_{0}^{*}$
110	61 109	syl	$⊢ φ \to \|\{x \in dom J \| N \in J (x)\}\| \in ℕ_{0}^{*}$
111		hashxnn0	$⊢ \{x \in dom I \| I (x) = \{N\}\} \in V \to \|\{x \in dom I \| I (x) = \{N\}\}\| \in ℕ_{0}^{*}$
112	93 111	syl	$⊢ φ \to \|\{x \in dom I \| I (x) = \{N\}\}\| \in ℕ_{0}^{*}$
113		hashxnn0	$⊢ \{x \in dom J \| J (x) = \{N\}\} \in V \to \|\{x \in dom J \| J (x) = \{N\}\}\| \in ℕ_{0}^{*}$
114	95 113	syl	$⊢ φ \to \|\{x \in dom J \| J (x) = \{N\}\}\| \in ℕ_{0}^{*}$
115	108 110 112 114	xnn0add4d	$⊢ φ \to (\|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom J \| N \in J (x)\}\|) +_{𝑒} (\|\{x \in dom I \| I (x) = \{N\}\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|) = (\|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom I \| I (x) = \{N\}\}\|) +_{𝑒} (\|\{x \in dom J \| N \in J (x)\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|)$
116	106 115	eqtrd	$⊢ φ \to \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\| = (\|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom I \| I (x) = \{N\}\}\|) +_{𝑒} (\|\{x \in dom J \| N \in J (x)\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|)$
117	9 5	eleqtrrd	$⊢ φ \to N \in Vtx (U)$
118		eqid	$⊢ Vtx (U) = Vtx (U)$
119		eqid	$⊢ iEdg (U) = iEdg (U)$
120		eqid	$⊢ dom iEdg (U) = dom iEdg (U)$
121	118 119 120	vtxdgval	$⊢ N \in Vtx (U) \to VtxDeg (U) (N) = \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\|$
122	117 121	syl	$⊢ φ \to VtxDeg (U) (N) = \|\{x \in dom iEdg (U) \| N \in iEdg (U) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (U) \| iEdg (U) (x) = \{N\}\}\|$
123		eqid	$⊢ dom I = dom I$
124	3 1 123	vtxdgval	$⊢ N \in V \to VtxDeg (G) (N) = \|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom I \| I (x) = \{N\}\}\|$
125	9 124	syl	$⊢ φ \to VtxDeg (G) (N) = \|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom I \| I (x) = \{N\}\}\|$
126	9 4	eleqtrrd	$⊢ φ \to N \in Vtx (H)$
127		eqid	$⊢ Vtx (H) = Vtx (H)$
128		eqid	$⊢ dom J = dom J$
129	127 2 128	vtxdgval	$⊢ N \in Vtx (H) \to VtxDeg (H) (N) = \|\{x \in dom J \| N \in J (x)\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|$
130	126 129	syl	$⊢ φ \to VtxDeg (H) (N) = \|\{x \in dom J \| N \in J (x)\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|$
131	125 130	oveq12d	$⊢ φ \to VtxDeg (G) (N) +_{𝑒} VtxDeg (H) (N) = (\|\{x \in dom I \| N \in I (x)\}\| +_{𝑒} \|\{x \in dom I \| I (x) = \{N\}\}\|) +_{𝑒} (\|\{x \in dom J \| N \in J (x)\}\| +_{𝑒} \|\{x \in dom J \| J (x) = \{N\}\}\|)$
132	116 122 131	3eqtr4d	$⊢ φ \to VtxDeg (U) (N) = VtxDeg (G) (N) +_{𝑒} VtxDeg (H) (N)$

Metamath Proof Explorer

Theorem vtxdun

Proof