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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion eulerpathpr ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )

Proof

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