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 ) ) |