vtxdgoddnumeven

Description: The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in Diestel p. 5. See also remark about equation (2) in section I.1 in Bollobas p. 4. (Contributed by AV, 22-Dec-2021)

	Ref	Expression
Hypotheses	finsumvtxdgeven.v	$⊢ V = Vtx (G)$
	finsumvtxdgeven.i	$⊢ I = iEdg (G)$
	finsumvtxdgeven.d	$⊢ D = VtxDeg (G)$
Assertion	vtxdgoddnumeven	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|$

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdgeven.v	$⊢ V = Vtx (G)$
2		finsumvtxdgeven.i	$⊢ I = iEdg (G)$
3		finsumvtxdgeven.d	$⊢ D = VtxDeg (G)$
4	1 2 3	finsumvtxdgeven	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \sum_{w \in V} D (w)$
5		incom	$⊢ \{v \in V \| \neg 2 ∥ D (v)\} \cap \{v \in V \| 2 ∥ D (v)\} = \{v \in V \| 2 ∥ D (v)\} \cap \{v \in V \| \neg 2 ∥ D (v)\}$
6		rabnc	$⊢ \{v \in V \| 2 ∥ D (v)\} \cap \{v \in V \| \neg 2 ∥ D (v)\} = \emptyset$
7	5 6	eqtri	$⊢ \{v \in V \| \neg 2 ∥ D (v)\} \cap \{v \in V \| 2 ∥ D (v)\} = \emptyset$
8	7	a1i	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \{v \in V \| \neg 2 ∥ D (v)\} \cap \{v \in V \| 2 ∥ D (v)\} = \emptyset$
9		rabxm	$⊢ V = \{v \in V \| 2 ∥ D (v)\} \cup \{v \in V \| \neg 2 ∥ D (v)\}$
10	9	equncomi	$⊢ V = \{v \in V \| \neg 2 ∥ D (v)\} \cup \{v \in V \| 2 ∥ D (v)\}$
11	10	a1i	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to V = \{v \in V \| \neg 2 ∥ D (v)\} \cup \{v \in V \| 2 ∥ D (v)\}$
12		simp2	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to V \in Fin$
13	3	fveq1i	$⊢ D (w) = VtxDeg (G) (w)$
14		dmfi	$⊢ I \in Fin \to dom I \in Fin$
15	14	3ad2ant3	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to dom I \in Fin$
16		eqid	$⊢ dom I = dom I$
17	1 2 16	vtxdgfisnn0	$⊢ (dom I \in Fin \land w \in V) \to VtxDeg (G) (w) \in ℕ_{0}$
18	15 17	sylan	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in V) \to VtxDeg (G) (w) \in ℕ_{0}$
19	18	nn0cnd	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in V) \to VtxDeg (G) (w) \in ℂ$
20	13 19	eqeltrid	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in V) \to D (w) \in ℂ$
21	8 11 12 20	fsumsplit	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \sum_{w \in V} D (w) = \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)$
22	21	breq2d	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (2 ∥ \sum_{w \in V} D (w) \leftrightarrow 2 ∥ (\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)))$
23		rabfi	$⊢ V \in Fin \to \{v \in V \| \neg 2 ∥ D (v)\} \in Fin$
24	23	3ad2ant2	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \{v \in V \| \neg 2 ∥ D (v)\} \in Fin$
25		elrabi	$⊢ w \in \{v \in V \| \neg 2 ∥ D (v)\} \to w \in V$
26	15 25 17	syl2an	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| \neg 2 ∥ D (v)\}) \to VtxDeg (G) (w) \in ℕ_{0}$
27	26	nn0zd	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| \neg 2 ∥ D (v)\}) \to VtxDeg (G) (w) \in ℤ$
28	13 27	eqeltrid	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| \neg 2 ∥ D (v)\}) \to D (w) \in ℤ$
29	24 28	fsumzcl	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) \in ℤ$
30	29	adantr	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land \neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|) \to \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) \in ℤ$
31		fveq2	$⊢ v = w \to D (v) = D (w)$
32	31	breq2d	$⊢ v = w \to (2 ∥ D (v) \leftrightarrow 2 ∥ D (w))$
33	32	notbid	$⊢ v = w \to (\neg 2 ∥ D (v) \leftrightarrow \neg 2 ∥ D (w))$
34	33	elrab	$⊢ w \in \{v \in V \| \neg 2 ∥ D (v)\} \leftrightarrow (w \in V \land \neg 2 ∥ D (w))$
35	34	simprbi	$⊢ w \in \{v \in V \| \neg 2 ∥ D (v)\} \to \neg 2 ∥ D (w)$
36	35	adantl	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| \neg 2 ∥ D (v)\}) \to \neg 2 ∥ D (w)$
37	24 28 36	sumodd	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\| \leftrightarrow 2 ∥ \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w))$
38	37	notbid	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (\neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\| \leftrightarrow \neg 2 ∥ \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w))$
39	38	biimpa	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land \neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|) \to \neg 2 ∥ \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w)$
40		rabfi	$⊢ V \in Fin \to \{v \in V \| 2 ∥ D (v)\} \in Fin$
41	40	3ad2ant2	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \{v \in V \| 2 ∥ D (v)\} \in Fin$
42		elrabi	$⊢ w \in \{v \in V \| 2 ∥ D (v)\} \to w \in V$
43	15 42 17	syl2an	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| 2 ∥ D (v)\}) \to VtxDeg (G) (w) \in ℕ_{0}$
44	43	nn0zd	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| 2 ∥ D (v)\}) \to VtxDeg (G) (w) \in ℤ$
45	13 44	eqeltrid	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| 2 ∥ D (v)\}) \to D (w) \in ℤ$
46	41 45	fsumzcl	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w) \in ℤ$
47	46	adantr	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land \neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|) \to \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w) \in ℤ$
48	32	elrab	$⊢ w \in \{v \in V \| 2 ∥ D (v)\} \leftrightarrow (w \in V \land 2 ∥ D (w))$
49	48	simprbi	$⊢ w \in \{v \in V \| 2 ∥ D (v)\} \to 2 ∥ D (w)$
50	49	adantl	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land w \in \{v \in V \| 2 ∥ D (v)\}) \to 2 ∥ D (w)$
51	41 45 50	sumeven	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)$
52	51	adantr	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land \neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|) \to 2 ∥ \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)$
53		opeo	$⊢ ((\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) \in ℤ \land \neg 2 ∥ \sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w)) \land (\sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w) \in ℤ \land 2 ∥ \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w))) \to \neg 2 ∥ (\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w))$
54	30 39 47 52 53	syl22anc	$⊢ ((G \in UPGraph \land V \in Fin \land I \in Fin) \land \neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|) \to \neg 2 ∥ (\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w))$
55	54	ex	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (\neg 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\| \to \neg 2 ∥ (\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)))$
56	55	con4d	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (2 ∥ (\sum_{w \in \{v \in V \| \neg 2 ∥ D (v)\}} D (w) + \sum_{w \in \{v \in V \| 2 ∥ D (v)\}} D (w)) \to 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|)$
57	22 56	sylbid	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to (2 ∥ \sum_{w \in V} D (w) \to 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|)$
58	4 57	mpd	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \|\{v \in V \| \neg 2 ∥ D (v)\}\|$

Metamath Proof Explorer

Theorem vtxdgoddnumeven

Proof