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

Metamath Proof Explorer

Theorem eupth2lem3

Description: Lemma 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 ‘ 𝐺 ) 𝑃 )
eupth2.h ⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩
eupth2.x ⊢ 𝑋 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩
eupth2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
eupth2.l ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) )
eupth2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
eupth2.o ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
Assertion eupth2lem3 ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )

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 eupth2.h ⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩
7 eupth2.x ⊢ 𝑋 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩
8 eupth2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 eupth2.l ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) )
10 eupth2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
11 eupth2.o ⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
12 eupthiswlk ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
13 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
14 5 12 13 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
15 nn0p1elfzo ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 8 14 9 15 syl3anc ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 eupthistrl ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
18 5 17 syl ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
19 6 fveq2i ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ )
20 1 fvexi ⊢ 𝑉 ∈ V
21 2 fvexi ⊢ 𝐼 ∈ V
22 21 resex ⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∈ V
23 20 22 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ ) = 𝑉
24 19 23 eqtri ⊢ ( Vtx ‘ 𝐻 ) = 𝑉
25 24 a1i ⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
26 snex ⊢ { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ∈ V
27 20 26 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = 𝑉
28 27 a1i ⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = 𝑉 )
29 7 fveq2i ⊢ ( Vtx ‘ 𝑋 ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ )
30 21 resex ⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ∈ V
31 20 30 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ ) = 𝑉
32 29 31 eqtri ⊢ ( Vtx ‘ 𝑋 ) = 𝑉
33 32 a1i ⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
34 6 fveq2i ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ )
35 20 22 opiedgfvi ⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
36 34 35 eqtri ⊢ ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
37 36 a1i ⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
38 20 26 opiedgfvi ⊢ ( iEdg ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ }
39 38 a1i ⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
40 7 fveq2i ⊢ ( iEdg ‘ 𝑋 ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ )
41 20 30 opiedgfvi ⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
42 40 41 eqtri ⊢ ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
43 8 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
44 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
45 44 eqcomd ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
46 43 45 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
47 46 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( 𝐹 “ ( 0 ... 𝑁 ) ) )
48 47 reseq2d ⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
49 42 48 eqtrid ⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
50 2fveq3 ⊢ ( 𝑘 = 𝑁 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )
51 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) )
52 fvoveq1 ⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
53 51 52 preq12d ⊢ ( 𝑘 = 𝑁 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
54 50 53 eqeq12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
55 5 12 syl ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
56 2 upgrwlkedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
57 3 55 56 syl2anc ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
58 54 57 16 rspcdva ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
59 1 2 4 16 10 18 25 28 33 37 39 49 11 58 eupth2lem3lem7 ⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )