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