Metamath Proof Explorer

Theorem eulerpathpr

Description: A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypothesis eulerpathpr.v ⊢ V = Vtx ⁡ G
Assertion eulerpathpr ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2

Proof

Step Hyp Ref Expression
1 eulerpathpr.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 simpl ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → G ∈ UPGraph
4 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
5 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
6 4 5 syl ⊢ G ∈ UPGraph → Fun ⁡ iEdg ⁡ G
7 6 adantr ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → Fun ⁡ iEdg ⁡ G
8 simpr ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → F EulerPaths ⁡ G P
9 1 2 3 7 8 eupth2 ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F
10 9 fveq2d ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F
11 fveq2 ⊢ ∅ = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F → ∅ = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F
12 11 eleq1d ⊢ ∅ = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F → ∅ ∈ 0 2 ↔ if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F ∈ 0 2
13 fveq2 ⊢ P ⁡ 0 P ⁡ F = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F → P ⁡ 0 P ⁡ F = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F
14 13 eleq1d ⊢ P ⁡ 0 P ⁡ F = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F → P ⁡ 0 P ⁡ F ∈ 0 2 ↔ if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F ∈ 0 2
15 hash0 ⊢ ∅ = 0
16 c0ex ⊢ 0 ∈ V
17 16 prid1 ⊢ 0 ∈ 0 2
18 15 17 eqeltri ⊢ ∅ ∈ 0 2
19 18 a1i ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → ∅ ∈ 0 2
20 simpr ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ ¬ P ⁡ 0 = P ⁡ F → ¬ P ⁡ 0 = P ⁡ F
21 20 neqned ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ ¬ P ⁡ 0 = P ⁡ F → P ⁡ 0 ≠ P ⁡ F
22 fvex ⊢ P ⁡ 0 ∈ V
23 fvex ⊢ P ⁡ F ∈ V
24 hashprg ⊢ P ⁡ 0 ∈ V ∧ P ⁡ F ∈ V → P ⁡ 0 ≠ P ⁡ F ↔ P ⁡ 0 P ⁡ F = 2
25 22 23 24 mp2an ⊢ P ⁡ 0 ≠ P ⁡ F ↔ P ⁡ 0 P ⁡ F = 2
26 21 25 sylib ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ ¬ P ⁡ 0 = P ⁡ F → P ⁡ 0 P ⁡ F = 2
27 2ex ⊢ 2 ∈ V
28 27 prid2 ⊢ 2 ∈ 0 2
29 26 28 eqeltrdi ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ ¬ P ⁡ 0 = P ⁡ F → P ⁡ 0 P ⁡ F ∈ 0 2
30 12 14 19 29 ifbothda ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F ∈ 0 2
31 10 30 eqeltrd ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ 0 2