Theorem erclwwlk

Description: .~ is an equivalence relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Hypothesis	erclwwlk.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨u,w⟩|\left(u\in \mathrm{ClWWalks}\left(G\right)\wedge w\in \mathrm{ClWWalks}\left(G\right)\wedge \exists n\in \left(0\dots \left|w\right|\right)u=w\mathrm{cyclShift}n\right)\right\}$$
Assertion	erclwwlk	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{ClWWalks}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨u,w⟩|\left(u\in \mathrm{ClWWalks}\left(G\right)\wedge w\in \mathrm{ClWWalks}\left(G\right)\wedge \exists n\in \left(0\dots \left|w\right|\right)u=w\mathrm{cyclShift}n\right)\right\}$$
2	1	erclwwlkrel	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$
3	1	erclwwlksym	$$⊢x\underset{\dot{}}{\sim }y\to y\underset{\dot{}}{\sim }x$$
4	1	erclwwlktr	$$⊢\left(x\underset{\dot{}}{\sim }y\wedge y\underset{\dot{}}{\sim }z\right)\to x\underset{\dot{}}{\sim }z$$
5	1	erclwwlkref	$$⊢x\in \mathrm{ClWWalks}\left(G\right)\leftrightarrow x\underset{\dot{}}{\sim }x$$
6	2 3 4 5	iseri	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{ClWWalks}\left(G\right)$$