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 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡𝑊𝑢𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion fusgrhashclwwlkn ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 / ) ) · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡𝑊𝑢𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 3 fusgrvtxfi ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin )
5 4 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
6 1 2 hashclwwlkn0 ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ♯ ‘ 𝑊 ) = Σ 𝑥 ∈ ( 𝑊 / ) ( ♯ ‘ 𝑥 ) )
7 5 6 syl ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑊 ) = Σ 𝑥 ∈ ( 𝑊 / ) ( ♯ ‘ 𝑥 ) )
8 fusgrusgr ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
9 usgrumgr ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
10 8 9 syl ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ UMGraph )
11 1 2 umgrhashecclwwlk ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑥 ∈ ( 𝑊 / ) → ( ♯ ‘ 𝑥 ) = 𝑁 ) )
12 10 11 sylan ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑥 ∈ ( 𝑊 / ) → ( ♯ ‘ 𝑥 ) = 𝑁 ) )
13 12 imp ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ ( 𝑊 / ) ) → ( ♯ ‘ 𝑥 ) = 𝑁 )
14 13 sumeq2dv ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → Σ 𝑥 ∈ ( 𝑊 / ) ( ♯ ‘ 𝑥 ) = Σ 𝑥 ∈ ( 𝑊 / ) 𝑁 )
15 1 2 qerclwwlknfi ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑊 / ) ∈ Fin )
16 5 15 syl ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑊 / ) ∈ Fin )
17 prmnn ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
18 17 nncnd ( 𝑁 ∈ ℙ → 𝑁 ∈ ℂ )
19 18 adantl ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℂ )
20 fsumconst ( ( ( 𝑊 / ) ∈ Fin ∧ 𝑁 ∈ ℂ ) → Σ 𝑥 ∈ ( 𝑊 / ) 𝑁 = ( ( ♯ ‘ ( 𝑊 / ) ) · 𝑁 ) )
21 16 19 20 syl2anc ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → Σ 𝑥 ∈ ( 𝑊 / ) 𝑁 = ( ( ♯ ‘ ( 𝑊 / ) ) · 𝑁 ) )
22 7 14 21 3eqtrd ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 / ) ) · 𝑁 ) )