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

Metamath Proof Explorer

Theorem trlsegvdeglem1

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
trlsegvdeg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
trlsegvdeg.f ⊢ ( 𝜑 → Fun 𝐼 )
trlsegvdeg.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
trlsegvdeg.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
trlsegvdeg.w ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
Assertion trlsegvdeglem1 ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 trlsegvdeg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 trlsegvdeg.f ⊢ ( 𝜑 → Fun 𝐼 )
4 trlsegvdeg.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 trlsegvdeg.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6 trlsegvdeg.w ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
7 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8 1 wlkpvtx ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ) )
9 elfzofz ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
10 8 9 impel ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 )
11 1 wlkpvtx ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )
12 fzofzp1 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 11 12 impel ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 )
14 10 13 jca ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )
15 14 ex ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) ) )
16 6 7 15 3syl ⊢ ( 𝜑 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) ) )
17 4 16 mpd ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )