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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion hashclwwlkn0
|- ( ( Vtx ` G ) e. Fin -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )

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 erclwwlkn
 |-  .~ Er W
4 3 a1i
 |-  ( ( Vtx ` G ) e. Fin -> .~ Er W )
5 clwwlknfi
 |-  ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin )
6 1 5 eqeltrid
 |-  ( ( Vtx ` G ) e. Fin -> W e. Fin )
7 4 6 qshash
 |-  ( ( Vtx ` G ) e. Fin -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )