Metamath Proof Explorer


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 W u W n 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 W u W n 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 W x ˙ x
7 3 4 5 6 iseri ˙ Er W