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 \in FinUSGraph \land N \in ℙ) \to N ∥ \|N ClWWalksN G\|$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	fusgrvtxfi	$⊢ G \in FinUSGraph \to Vtx (G) \in Fin$
3	2	adantr	$⊢ (G \in FinUSGraph \land N \in ℙ) \to Vtx (G) \in Fin$
4		eqid	$⊢ N ClWWalksN G = N ClWWalksN G$
5		eqid	$⊢ \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\} = \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
6	4 5	qerclwwlknfi	$⊢ Vtx (G) \in Fin \to (N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\} \in Fin$
7		hashcl	$⊢ (N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\} \in Fin \to \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \in ℕ_{0}$
8	3 6 7	3syl	$⊢ (G \in FinUSGraph \land N \in ℙ) \to \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \in ℕ_{0}$
9	8	nn0zd	$⊢ (G \in FinUSGraph \land N \in ℙ) \to \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \in ℤ$
10		prmz	$⊢ N \in ℙ \to N \in ℤ$
11	10	adantl	$⊢ (G \in FinUSGraph \land N \in ℙ) \to N \in ℤ$
12		dvdsmul2	$⊢ (\|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \in ℤ \land N \in ℤ) \to N ∥ \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \cdot N$
13	9 11 12	syl2anc	$⊢ (G \in FinUSGraph \land N \in ℙ) \to N ∥ \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \cdot N$
14	4 5	fusgrhashclwwlkn	$⊢ (G \in FinUSGraph \land N \in ℙ) \to \|N ClWWalksN G\| = \|(N ClWWalksN G) / \{⟨t, u⟩ \| (t \in (N ClWWalksN G) \land u \in (N ClWWalksN G) \land \exists n \in (0 \dots N) t = u cyclShift n)\}\| \cdot N$
15	13 14	breqtrrd	$⊢ (G \in FinUSGraph \land N \in ℙ) \to N ∥ \|N ClWWalksN G\|$