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