Metamath Proof Explorer

Theorem 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 ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ v ∈ V | ¬ 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 ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ w ∈ V D ⁡ w
5 incom ⊢ v ∈ V | ¬ 2 ∥ D ⁡ v ∩ v ∈ V | 2 ∥ D ⁡ v = v ∈ V | 2 ∥ D ⁡ v ∩ v ∈ V | ¬ 2 ∥ D ⁡ v
6 rabnc ⊢ v ∈ V | 2 ∥ D ⁡ v ∩ v ∈ V | ¬ 2 ∥ D ⁡ v = ∅
7 5 6 eqtri ⊢ v ∈ V | ¬ 2 ∥ D ⁡ v ∩ v ∈ V | 2 ∥ D ⁡ v = ∅
8 7 a1i ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → v ∈ V | ¬ 2 ∥ D ⁡ v ∩ v ∈ V | 2 ∥ D ⁡ v = ∅
9 rabxm ⊢ V = v ∈ V | 2 ∥ D ⁡ v ∪ v ∈ V | ¬ 2 ∥ D ⁡ v
10 9 equncomi ⊢ V = v ∈ V | ¬ 2 ∥ D ⁡ v ∪ v ∈ V | 2 ∥ D ⁡ v
11 10 a1i ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → V = v ∈ V | ¬ 2 ∥ D ⁡ v ∪ v ∈ V | 2 ∥ D ⁡ v
12 simp2 ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → V ∈ Fin
13 3 fveq1i ⊢ D ⁡ w = VtxDeg ⁡ G ⁡ w
14 dmfi ⊢ I ∈ Fin → dom ⁡ I ∈ Fin
15 14 3ad2ant3 ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → dom ⁡ I ∈ Fin
16 eqid ⊢ dom ⁡ I = dom ⁡ I
17 1 2 16 vtxdgfisnn0 ⊢ dom ⁡ I ∈ Fin ∧ w ∈ V → VtxDeg ⁡ G ⁡ w ∈ ℕ 0
18 15 17 sylan ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ V → VtxDeg ⁡ G ⁡ w ∈ ℕ 0
19 18 nn0cnd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ V → VtxDeg ⁡ G ⁡ w ∈ ℂ
20 13 19 eqeltrid ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ V → D ⁡ w ∈ ℂ
21 8 11 12 20 fsumsplit ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ∑ w ∈ V D ⁡ w = ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
22 21 breq2d ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ w ∈ V D ⁡ w ↔ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
23 rabfi ⊢ V ∈ Fin → v ∈ V | ¬ 2 ∥ D ⁡ v ∈ Fin
24 23 3ad2ant2 ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → v ∈ V | ¬ 2 ∥ D ⁡ v ∈ Fin
25 elrabi ⊢ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → w ∈ V
26 15 25 17 syl2an ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → VtxDeg ⁡ G ⁡ w ∈ ℕ 0
27 26 nn0zd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → VtxDeg ⁡ G ⁡ w ∈ ℤ
28 13 27 eqeltrid ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → D ⁡ w ∈ ℤ
29 24 28 fsumzcl ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w ∈ ℤ
30 29 adantr ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w ∈ ℤ
31 fveq2 ⊢ v = w → D ⁡ v = D ⁡ w
32 31 breq2d ⊢ v = w → 2 ∥ D ⁡ v ↔ 2 ∥ D ⁡ w
33 32 notbid ⊢ v = w → ¬ 2 ∥ D ⁡ v ↔ ¬ 2 ∥ D ⁡ w
34 33 elrab ⊢ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v ↔ w ∈ V ∧ ¬ 2 ∥ D ⁡ w
35 34 simprbi ⊢ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → ¬ 2 ∥ D ⁡ w
36 35 adantl ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v → ¬ 2 ∥ D ⁡ w
37 24 28 36 sumodd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v ↔ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w
38 37 notbid ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v ↔ ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w
39 38 biimpa ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w
40 rabfi ⊢ V ∈ Fin → v ∈ V | 2 ∥ D ⁡ v ∈ Fin
41 40 3ad2ant2 ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → v ∈ V | 2 ∥ D ⁡ v ∈ Fin
42 elrabi ⊢ w ∈ v ∈ V | 2 ∥ D ⁡ v → w ∈ V
43 15 42 17 syl2an ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | 2 ∥ D ⁡ v → VtxDeg ⁡ G ⁡ w ∈ ℕ 0
44 43 nn0zd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | 2 ∥ D ⁡ v → VtxDeg ⁡ G ⁡ w ∈ ℤ
45 13 44 eqeltrid ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | 2 ∥ D ⁡ v → D ⁡ w ∈ ℤ
46 41 45 fsumzcl ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w ∈ ℤ
47 46 adantr ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w ∈ ℤ
48 32 elrab ⊢ w ∈ v ∈ V | 2 ∥ D ⁡ v ↔ w ∈ V ∧ 2 ∥ D ⁡ w
49 48 simprbi ⊢ w ∈ v ∈ V | 2 ∥ D ⁡ v → 2 ∥ D ⁡ w
50 49 adantl ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ w ∈ v ∈ V | 2 ∥ D ⁡ v → 2 ∥ D ⁡ w
51 41 45 50 sumeven ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
52 51 adantr ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → 2 ∥ ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
53 opeo ⊢ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w ∈ ℤ ∧ ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w ∧ ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w ∈ ℤ ∧ 2 ∥ ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w → ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
54 30 39 47 52 53 syl22anc ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin ∧ ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
55 54 ex ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ¬ 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v → ¬ 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w
56 55 con4d ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ w ∈ v ∈ V | ¬ 2 ∥ D ⁡ v D ⁡ w + ∑ w ∈ v ∈ V | 2 ∥ D ⁡ v D ⁡ w → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v
57 22 56 sylbid ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ w ∈ V D ⁡ w → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v
58 4 57 mpd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v