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	|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion	erclwwlk	|- .~ Er ( ClWWalks ` G )

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
2	1	erclwwlkrel	|- Rel .~
3	1	erclwwlksym	|- ( x .~ y -> y .~ x )
4	1	erclwwlktr	|- ( ( x .~ y /\ y .~ z ) -> x .~ z )
5	1	erclwwlkref	|- ( x e. ( ClWWalks ` G ) <-> x .~ x )
6	2 3 4 5	iseri	|- .~ Er ( ClWWalks ` G )