Theorem cyclispthon

Description: A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	cyclispthon	$$⊢F\mathrm{Cycles}\left(G\right)P\to F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(0\right)\right)P$$

Proof

Step	Hyp	Ref	Expression
1		cyclispth	$$⊢F\mathrm{Cycles}\left(G\right)P\to F\mathrm{Paths}\left(G\right)P$$
2		pthonpth	$$⊢F\mathrm{Paths}\left(G\right)P\to F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(\left|F\right|\right)\right)P$$
3	1 2	syl	$$⊢F\mathrm{Cycles}\left(G\right)P\to F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(\left|F\right|\right)\right)P$$
4		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)$$
5	4	simprbi	$$⊢F\mathrm{Cycles}\left(G\right)P\to P\left(0\right)=P\left(\left|F\right|\right)$$
6	5	oveq2d	$$⊢F\mathrm{Cycles}\left(G\right)P\to P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(0\right)=P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(\left|F\right|\right)$$
7	6	breqd	$$⊢F\mathrm{Cycles}\left(G\right)P\to \left(F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(0\right)\right)P\leftrightarrow F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(\left|F\right|\right)\right)P\right)$$
8	3 7	mpbird	$$⊢F\mathrm{Cycles}\left(G\right)P\to F\left(P\left(0\right)\mathrm{PathsOn}\left(G\right)P\left(0\right)\right)P$$