Metamath Proof Explorer


Theorem fusgrhashclwwlkn

Description: The size of the set of closed walks (defined as words) with a fixed length which is a prime number is the product of the number of equivalence classes for .~ over the set of closed walks and the fixed length. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 1-May-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 fusgrhashclwwlkn G FinUSGraph N W = W / ˙ N

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 eqid Vtx G = Vtx G
4 3 fusgrvtxfi G FinUSGraph Vtx G Fin
5 4 adantr G FinUSGraph N Vtx G Fin
6 1 2 hashclwwlkn0 Vtx G Fin W = x W / ˙ x
7 5 6 syl G FinUSGraph N W = x W / ˙ x
8 fusgrusgr G FinUSGraph G USGraph
9 usgrumgr G USGraph G UMGraph
10 8 9 syl G FinUSGraph G UMGraph
11 1 2 umgrhashecclwwlk G UMGraph N x W / ˙ x = N
12 10 11 sylan G FinUSGraph N x W / ˙ x = N
13 12 imp G FinUSGraph N x W / ˙ x = N
14 13 sumeq2dv G FinUSGraph N x W / ˙ x = x W / ˙ N
15 1 2 qerclwwlknfi Vtx G Fin W / ˙ Fin
16 5 15 syl G FinUSGraph N W / ˙ Fin
17 prmnn N N
18 17 nncnd N N
19 18 adantl G FinUSGraph N N
20 fsumconst W / ˙ Fin N x W / ˙ N = W / ˙ N
21 16 19 20 syl2anc G FinUSGraph N x W / ˙ N = W / ˙ N
22 7 14 21 3eqtrd G FinUSGraph N W = W / ˙ N