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 ) ) ∈ 𝑉 ) )