Theorem wlklenvp1

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\mathrm{Walks}\left(G\right)P\to \left|P\right|=\left|F\right|+1$$

Proof

Step	Hyp	Ref	Expression
1		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
2		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
3	2	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)$$
4		ffz0hash	$$⊢\left(\left|F\right|\in {\mathbb{N}}_0\wedge P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\right)\to \left|P\right|=\left|F\right|+1$$
5	1 3 4	syl2anc	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|P\right|=\left|F\right|+1$$