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 ⊢ V = Vtx ⁡ G
Assertion numclwwlk6 ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ P ∈ ℙ ∧ P ∥ K − 1 → P ClWWalksN G mod P = V mod P

Proof

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