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 biimtrdi ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
21 10 20 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )