Metamath Proof Explorer

Theorem wlklenvm1

Description: The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlklenvm1 
|- ( F ( Walks ` G ) P -> ( # ` F ) = ( ( # ` P ) - 1 ) )

Proof

Step Hyp Ref Expression
1 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
2 oveq1 
 |-  ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` F ) + 1 ) - 1 ) )
3 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
4 3 nn0cnd 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. CC )
5 pncan1 
 |-  ( ( # ` F ) e. CC -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
6 4 5 syl 
 |-  ( F ( Walks ` G ) P -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
7 2 6 sylan9eqr 
 |-  ( ( F ( Walks ` G ) P /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) )
8 7 eqcomd 
 |-  ( ( F ( Walks ` G ) P /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
9 1 8 mpdan 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) = ( ( # ` P ) - 1 ) )