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

Metamath Proof Explorer

Theorem clwwlkndivn

Description: The size of the set of closed walks (defined as words) of length N is divisible by N if N is a prime number. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 2-May-2021)

Ref Expression
Assertion clwwlkndivn ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 fusgrvtxfi ⊢ ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin )
3 2 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( Vtx ‘ 𝐺 ) ∈ Fin )
4 eqid ⊢ ( 𝑁 ClWWalksN 𝐺 ) = ( 𝑁 ClWWalksN 𝐺 )
5 eqid ⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
6 4 5 qerclwwlknfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ∈ Fin )
7 hashcl ⊢ ( ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ∈ Fin → ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) ∈ ℕ0 )
8 3 6 7 3syl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) ∈ ℕ0 )
9 8 nn0zd ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) ∈ ℤ )
10 prmz ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℤ )
11 10 adantl ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℤ )
12 dvdsmul2 ⊢ ( ( ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) · 𝑁 ) )
13 9 11 12 syl2anc ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) · 𝑁 ) )
14 4 5 fusgrhashclwwlkn ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) = ( ( ♯ ‘ ( ( 𝑁 ClWWalksN 𝐺 ) / { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) } ) ) · 𝑁 ) )
15 13 14 breqtrrd ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∥ ( ♯ ‘ ( 𝑁 ClWWalksN 𝐺 ) ) )