Metamath Proof Explorer

Theorem eulercrct

Description: A pseudograph with an Eulerian circuit <. F , P >. (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021)

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

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 3adant3 ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F
11 crctprop ⊢ F Circuits ⁡ G P → F Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ F
12 11 simprd ⊢ F Circuits ⁡ G P → P ⁡ 0 = P ⁡ F
13 12 3ad2ant3 ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → P ⁡ 0 = P ⁡ F
14 13 iftrued ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F = ∅
15 14 eqeq2d ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F ↔ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = ∅
16 rabeq0 ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = ∅ ↔ ∀ x ∈ V ¬ ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
17 notnotr ⊢ ¬ ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → 2 ∥ VtxDeg ⁡ G ⁡ x
18 17 ralimi ⊢ ∀ x ∈ V ¬ ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → ∀ x ∈ V 2 ∥ VtxDeg ⁡ G ⁡ x
19 16 18 sylbi ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = ∅ → ∀ x ∈ V 2 ∥ VtxDeg ⁡ G ⁡ x
20 15 19 biimtrdi ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x = if P ⁡ 0 = P ⁡ F ∅ P ⁡ 0 P ⁡ F → ∀ x ∈ V 2 ∥ VtxDeg ⁡ G ⁡ x
21 10 20 mpd ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ F Circuits ⁡ G P → ∀ x ∈ V 2 ∥ VtxDeg ⁡ G ⁡ x