Theorem wlkf

Description: The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021)

	Ref	Expression
Hypothesis	wlkf.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
Assertion	wlkf	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$

Proof

Step	Hyp	Ref	Expression
1		wlkf.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
3	2 1	wlkprop	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(F\in \mathrm{Word}\mathrm{dom}I\wedge P:\left(0\dots \left|F\right|\right)⟶\mathrm{Vtx}\left(G\right)\wedge \forall k\in \left(0..^\left|F\right|\right)if-\left(P\left(k\right)=P\left(k+1\right),I\left(F\left(k\right)\right)=\left\{P\left(k\right)\right\},\left\{P\left(k\right),P\left(k+1\right)\right\}\subseteq I\left(F\left(k\right)\right)\right)\right)$$
4	3	simp1d	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$