Theorem iscycl

Description: Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

	Ref	Expression
Assertion	iscycl	$$⊢F\mathrm{Cycles}\left(G\right)P\leftrightarrow \left(F\mathrm{Paths}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cycls	$$⊢\mathrm{Cycles}\left(G\right)=\left\{⟨f,p⟩|\left(f\mathrm{Paths}\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		relpths	$$⊢\mathrm{Rel}\mathrm{Paths}\left(G\right)$$
10	1 8 9	brfvopabrbr	$$⊢F\mathrm{Cycles}\left(G\right)P\leftrightarrow \left(F\mathrm{Paths}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)$$