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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion eulercrct ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )

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 3adant3 ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) )
11 crctprop ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
12 11 simprd ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
13 12 3ad2ant3 ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
14 13 iftrued ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) = ∅ )
15 14 eqeq2d ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ↔ { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ ) )
16 rabeq0 ( { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑥𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
17 notnotr ( ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) → 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
18 17 ralimi ( ∀ 𝑥𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) → ∀ 𝑥𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
19 16 18 sylbi ( { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ → ∀ 𝑥𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
20 15 19 syl6bi ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) → ∀ 𝑥𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
21 10 20 mpd ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )