This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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