Description: The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018) (Revised by AV, 1-May-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | wlklenvp1 | |- ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkcl | |- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 ) |
|
2 | eqid | |- ( Vtx ` G ) = ( Vtx ` G ) |
|
3 | 2 | wlkp | |- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
4 | ffz0hash | |- ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
|
5 | 1 3 4 | syl2anc | |- ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |