Metamath Proof Explorer

Theorem wlkonwlk

Description: A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 31-Jan-2021)

Ref Expression
Assertion wlkonwlk 
|- ( F ( Walks ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( F ( Walks ` G ) P -> F ( Walks ` G ) P )
2 eqidd 
 |-  ( F ( Walks ` G ) P -> ( P ` 0 ) = ( P ` 0 ) )
3 eqidd 
 |-  ( F ( Walks ` G ) P -> ( P ` ( # ` F ) ) = ( P ` ( # ` F ) ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 wlkepvtx 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) )
6 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
7 3simpc 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
8 6 7 syl 
 |-  ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) )
9 4 iswlkon 
 |-  ( ( ( ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 0 ) /\ ( P ` ( # ` F ) ) = ( P ` ( # ` F ) ) ) ) )
10 5 8 9 syl2anc 
 |-  ( F ( Walks ` G ) P -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 0 ) /\ ( P ` ( # ` F ) ) = ( P ` ( # ` F ) ) ) ) )
11 1 2 3 10 mpbir3and 
 |-  ( F ( Walks ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P )