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

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 ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 / ∼ ) ) · 𝑁 ) )