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 ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ N ClWWalksN G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → Vtx ⁡ G ∈ Fin
3 2 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → Vtx ⁡ G ∈ Fin
4 eqid ⊢ N ClWWalksN G = N ClWWalksN G
5 eqid ⊢ t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n = t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n
6 4 5 qerclwwlknfi ⊢ Vtx ⁡ G ∈ Fin → N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ Fin
7 hashcl ⊢ N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ Fin → N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ ℕ 0
8 3 6 7 3syl ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ ℕ 0
9 8 nn0zd ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ ℤ
10 prmz ⊢ N ∈ ℙ → N ∈ ℤ
11 10 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∈ ℤ
12 dvdsmul2 ⊢ N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ∈ ℤ ∧ N ∈ ℤ → N ∥ N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ⋅ N
13 9 11 12 syl2anc ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ⋅ N
14 4 5 fusgrhashclwwlkn ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ClWWalksN G = N ClWWalksN G / t u | t ∈ N ClWWalksN G ∧ u ∈ N ClWWalksN G ∧ ∃ n ∈ 0 … N t = u cyclShift n ⋅ N
15 13 14 breqtrrd ⊢ G ∈ FinUSGraph ∧ N ∈ ℙ → N ∥ N ClWWalksN G