Metamath Proof Explorer


Theorem hashclwwlkn0

Description: The number of closed walks (defined as words) with a fixed length is the sum of the sizes of all equivalence classes according to .~ . (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 hashclwwlkn0 Vtx G Fin W = x W / ˙ x

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 erclwwlkn ˙ Er W
4 3 a1i Vtx G Fin ˙ Er W
5 clwwlknfi Vtx G Fin N ClWWalksN G Fin
6 1 5 eqeltrid Vtx G Fin W Fin
7 4 6 qshash Vtx G Fin W = x W / ˙ x