This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupth2lemb

Description: Lemma for eupth2 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypotheses eupth2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
eupth2.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
eupth2.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
eupth2.f ⊢ ( 𝜑 → Fun 𝐼 )
eupth2.p ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
Assertion eupth2lemb ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ )

Proof

Step Hyp Ref Expression
1 eupth2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eupth2.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 eupth2.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
4 eupth2.f ⊢ ( 𝜑 → Fun 𝐼 )
5 eupth2.p ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
6 z0even ⊢ 2 ∥ 0
7 1 fvexi ⊢ 𝑉 ∈ V
8 2 fvexi ⊢ 𝐼 ∈ V
9 8 resex ⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V
10 7 9 pm3.2i ⊢ ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V )
11 opvtxfv ⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = 𝑉 )
12 10 11 mp1i ⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = 𝑉 )
13 12 eqcomd ⊢ ( 𝜑 → 𝑉 = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) )
14 13 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ) )
15 14 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) )
16 opiedgfv ⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) )
17 10 16 mp1i ⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) )
18 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
19 18 imaeq2i ⊢ ( 𝐹 “ ( 0 ..^ 0 ) ) = ( 𝐹 “ ∅ )
20 ima0 ⊢ ( 𝐹 “ ∅ ) = ∅
21 19 20 eqtri ⊢ ( 𝐹 “ ( 0 ..^ 0 ) ) = ∅
22 21 reseq2i ⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) = ( 𝐼 ↾ ∅ )
23 res0 ⊢ ( 𝐼 ↾ ∅ ) = ∅
24 22 23 eqtri ⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) = ∅
25 17 24 eqtrdi ⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ )
27 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ )
28 eqid ⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ )
29 27 28 vtxdg0e ⊢ ( ( 𝑥 ∈ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ∧ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) = ∅ ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) = 0 )
30 15 26 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) = 0 )
31 6 30 breqtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
32 31 notnotd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
34 rabeq0 ⊢ ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) )
35 33 34 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 0 ) ) ) ⟩ ) ‘ 𝑥 ) } = ∅ )