Metamath Proof Explorer

Theorem wlkonwlk1l

Description: A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkonwlk1l.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
Assertion wlkonwlk1l ( 𝜑 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( lastS ‘ 𝑃 ) ) 𝑃 )

Proof

Step Hyp Ref Expression
1 wlkonwlk1l.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2 eqidd ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
3 wlklenvm1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
4 3 fveq2d ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
5 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6 5 wlkpwrd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
7 lsw ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
8 6 7 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
9 4 8 eqtr4d ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )
10 1 9 syl ⊢ ( 𝜑 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) )
11 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
12 nn0p1nn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ )
13 11 12 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ )
14 wlklenvp1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
15 13 6 14 jca32 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) )
16 fstwrdne0 ⊢ ( ( ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
17 lswlgt0cl ⊢ ( ( ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) → ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) )
18 16 17 jca ⊢ ( ( ( ( ♯ ‘ 𝐹 ) + 1 ) ∈ ℕ ∧ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) ) )
19 15 18 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) ) )
20 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
21 20 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
22 wrdv ⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 ∈ Word V )
23 21 22 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word V )
24 19 23 6 jca32 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ) )
25 1 24 syl ⊢ ( 𝜑 → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ) )
26 5 iswlkon ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( lastS ‘ 𝑃 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( lastS ‘ 𝑃 ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) ) ) )
27 25 26 syl ⊢ ( 𝜑 → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( lastS ‘ 𝑃 ) ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( lastS ‘ 𝑃 ) ) ) )
28 1 2 10 27 mpbir3and ⊢ ( 𝜑 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( lastS ‘ 𝑃 ) ) 𝑃 )