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 )