Theorem isclwlk

Description: A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 16-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	isclwlk	$$⊢F\mathrm{ClWalks}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		clwlks	$$⊢\mathrm{ClWalks}\left(G\right)=\left\{⟨f,p⟩|\left(f\mathrm{Walks}\left(G\right)p\wedge p\left(0\right)=p\left(\left|f\right|\right)\right)\right\}$$
2		fveq1	$$⊢p=P\to p\left(0\right)=P\left(0\right)$$
3	2	adantl	$$⊢\left(f=F\wedge p=P\right)\to p\left(0\right)=P\left(0\right)$$
4		simpr	$$⊢\left(f=F\wedge p=P\right)\to p=P$$
5		fveq2	$$⊢f=F\to \left|f\right|=\left|F\right|$$
6	5	adantr	$$⊢\left(f=F\wedge p=P\right)\to \left|f\right|=\left|F\right|$$
7	4 6	fveq12d	$$⊢\left(f=F\wedge p=P\right)\to p\left(\left|f\right|\right)=P\left(\left|F\right|\right)$$
8	3 7	eqeq12d	$$⊢\left(f=F\wedge p=P\right)\to \left(p\left(0\right)=p\left(\left|f\right|\right)\leftrightarrow P\left(0\right)=P\left(\left|F\right|\right)\right)$$
9		relwlk	$$⊢\mathrm{Rel}\mathrm{Walks}\left(G\right)$$
10	1 8 9	brfvopabrbr	$$⊢F\mathrm{ClWalks}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)$$