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 
|- ( ph -> F ( Walks ` G ) P )
Assertion wlkonwlk1l 
|- ( ph -> F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P )

Proof

Step Hyp Ref Expression
1 wlkonwlk1l.w 
 |-  ( ph -> F ( Walks ` G ) P )
2 eqidd 
 |-  ( ph -> ( P ` 0 ) = ( P ` 0 ) )
3 wlklenvm1 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) = ( ( # ` P ) - 1 ) )
4 3 fveq2d 
 |-  ( F ( Walks ` G ) P -> ( P ` ( # ` F ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 5 wlkpwrd 
 |-  ( F ( Walks ` G ) P -> P e. Word ( Vtx ` G ) )
7 lsw 
 |-  ( P e. Word ( Vtx ` G ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
8 6 7 syl 
 |-  ( F ( Walks ` G ) P -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
9 4 8 eqtr4d 
 |-  ( F ( Walks ` G ) P -> ( P ` ( # ` F ) ) = ( lastS ` P ) )
10 1 9 syl 
 |-  ( ph -> ( P ` ( # ` F ) ) = ( lastS ` P ) )
11 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
12 nn0p1nn 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) + 1 ) e. NN )
13 11 12 syl 
 |-  ( F ( Walks ` G ) P -> ( ( # ` F ) + 1 ) e. NN )
14 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
15 13 6 14 jca32 
 |-  ( F ( Walks ` G ) P -> ( ( ( # ` F ) + 1 ) e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) ) )
16 fstwrdne0 
 |-  ( ( ( ( # ` F ) + 1 ) e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) ) -> ( P ` 0 ) e. ( Vtx ` G ) )
17 lswlgt0cl 
 |-  ( ( ( ( # ` F ) + 1 ) e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) ) -> ( lastS ` P ) e. ( Vtx ` G ) )
18 16 17 jca 
 |-  ( ( ( ( # ` F ) + 1 ) e. NN /\ ( P e. Word ( Vtx ` G ) /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) ) -> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( lastS ` P ) e. ( Vtx ` G ) ) )
19 15 18 syl 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( lastS ` P ) e. ( Vtx ` G ) ) )
20 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
21 20 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
22 wrdv 
 |-  ( F e. Word dom ( iEdg ` G ) -> F e. Word _V )
23 21 22 syl 
 |-  ( F ( Walks ` G ) P -> F e. Word _V )
24 19 23 6 jca32 
 |-  ( F ( Walks ` G ) P -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( lastS ` P ) e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word ( Vtx ` G ) ) ) )
25 1 24 syl 
 |-  ( ph -> ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( lastS ` P ) e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word ( Vtx ` G ) ) ) )
26 5 iswlkon 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( lastS ` P ) e. ( Vtx ` G ) ) /\ ( F e. Word _V /\ P e. Word ( Vtx ` G ) ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 0 ) /\ ( P ` ( # ` F ) ) = ( lastS ` P ) ) ) )
27 25 26 syl 
 |-  ( ph -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 0 ) /\ ( P ` ( # ` F ) ) = ( lastS ` P ) ) ) )
28 1 2 10 27 mpbir3and 
 |-  ( ph -> F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P )