Metamath Proof Explorer

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 𝑃 ) )