Theorem erclwwlkn

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

	Ref	Expression
Hypotheses	erclwwlkn.w	|- W = ( N ClWWalksN G )
	erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion	erclwwlkn	|- .~ Er W

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	|- W = ( N ClWWalksN G )
2		erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3	1 2	erclwwlknrel	|- Rel .~
4	1 2	erclwwlknsym	|- ( x .~ y -> y .~ x )
5	1 2	erclwwlkntr	|- ( ( x .~ y /\ y .~ z ) -> x .~ z )
6	1 2	erclwwlknref	|- ( x e. W <-> x .~ x )
7	3 4 5 6	iseri	|- .~ Er W