Theorem numclwwlk6

Description: For a prime divisor P of K - 1 , the total number of closed walks of length P in a K-regular friendship graph is equal modulo P to the number of vertices. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 3-Jun-2021) (Proof shortened by AV, 7-Mar-2022)

	Ref	Expression
Hypothesis	numclwwlk6.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	numclwwlk6	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk6.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	finrusgrfusgr	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
3	2	3adant2	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
4		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
5	4	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) → 𝑃 ∈ ℕ )
6	1	numclwwlk4	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑃 ∈ ℕ ) → ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) )
7	3 5 6	syl2an	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) = Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) )
8	7	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) )
9	5	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∈ ℕ )
10		simp3	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → 𝑉 ∈ Fin )
11	10	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑉 ∈ Fin )
12	11	adantr	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑉 ∈ Fin )
13	1	clwwlknonfin	⊢ ( 𝑉 ∈ Fin → ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ∈ Fin )
14		hashcl	⊢ ( ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ∈ Fin → ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) ∈ ℕ0 )
15	12 13 14	3syl	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) ∈ ℕ0 )
16	15	nn0zd	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) ∈ ℤ )
17	16	ralrimiva	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) ∈ ℤ )
18	9 11 17	modfsummod	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = ( Σ 𝑥 ∈ 𝑉 ( ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) mod 𝑃 ) )
19		simpl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) )
20		simpr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) )
21	20	anim1ci	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) )
22		3anass	⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) )
23	21 22	sylibr	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) )
24	1	numclwwlk5	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = 1 )
25	19 23 24	syl2an2r	⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = 1 )
26	25	sumeq2dv	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → Σ 𝑥 ∈ 𝑉 ( ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = Σ 𝑥 ∈ 𝑉 1 )
27	26	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( Σ 𝑥 ∈ 𝑉 ( ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) mod 𝑃 ) = ( Σ 𝑥 ∈ 𝑉 1 mod 𝑃 ) )
28	18 27	eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( Σ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝑥 ( ClWWalksNOn ‘ 𝐺 ) 𝑃 ) ) mod 𝑃 ) = ( Σ 𝑥 ∈ 𝑉 1 mod 𝑃 ) )
29		1cnd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) → 1 ∈ ℂ )
30		fsumconst	⊢ ( ( 𝑉 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑥 ∈ 𝑉 1 = ( ( ♯ ‘ 𝑉 ) · 1 ) )
31	10 29 30	syl2an	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → Σ 𝑥 ∈ 𝑉 1 = ( ( ♯ ‘ 𝑉 ) · 1 ) )
32		hashcl	⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
33	32	nn0red	⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℝ )
34		ax-1rid	⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℝ → ( ( ♯ ‘ 𝑉 ) · 1 ) = ( ♯ ‘ 𝑉 ) )
35	33 34	syl	⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) · 1 ) = ( ♯ ‘ 𝑉 ) )
36	35	3ad2ant3	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( ( ♯ ‘ 𝑉 ) · 1 ) = ( ♯ ‘ 𝑉 ) )
37	36	adantr	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ 𝑉 ) · 1 ) = ( ♯ ‘ 𝑉 ) )
38	31 37	eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → Σ 𝑥 ∈ 𝑉 1 = ( ♯ ‘ 𝑉 ) )
39	38	oveq1d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( Σ 𝑥 ∈ 𝑉 1 mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )
40	8 28 39	3eqtrd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )