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 \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|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 \land V \in Fin) \to G \in FinUSGraph$
3	2	3adant2	$⊢ (G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to G \in FinUSGraph$
4		prmnn	$⊢ P \in ℙ \to P \in ℕ$
5	4	adantr	$⊢ (P \in ℙ \land P ∥ (K - 1)) \to P \in ℕ$
6	1	numclwwlk4	$⊢ (G \in FinUSGraph \land P \in ℕ) \to \|P ClWWalksN G\| = \sum_{x \in V} \|x ClWWalksNOn (G) P\|$
7	3 5 6	syl2an	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| = \sum_{x \in V} \|x ClWWalksNOn (G) P\|$
8	7	oveq1d	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = \sum_{x \in V} \|x ClWWalksNOn (G) P\| \mod P$
9	5	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to P \in ℕ$
10		simp3	$⊢ (G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to V \in Fin$
11	10	adantr	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to V \in Fin$
12	11	adantr	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to V \in Fin$
13	1	clwwlknonfin	$⊢ V \in Fin \to x ClWWalksNOn (G) P \in Fin$
14		hashcl	$⊢ x ClWWalksNOn (G) P \in Fin \to \|x ClWWalksNOn (G) P\| \in ℕ_{0}$
15	12 13 14	3syl	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to \|x ClWWalksNOn (G) P\| \in ℕ_{0}$
16	15	nn0zd	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to \|x ClWWalksNOn (G) P\| \in ℤ$
17	16	ralrimiva	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \forall x \in V \|x ClWWalksNOn (G) P\| \in ℤ$
18	9 11 17	modfsummod	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} \|x ClWWalksNOn (G) P\| \mod P = \sum_{x \in V} (\|x ClWWalksNOn (G) P\| \mod P) \mod P$
19		simpl	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (G RegUSGraph K \land G \in FriendGraph \land V \in Fin)$
20		simpr	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to (P \in ℙ \land P ∥ (K - 1))$
21	20	anim1ci	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to (x \in V \land (P \in ℙ \land P ∥ (K - 1)))$
22		3anass	$⊢ (x \in V \land P \in ℙ \land P ∥ (K - 1)) \leftrightarrow (x \in V \land (P \in ℙ \land P ∥ (K - 1)))$
23	21 22	sylibr	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to (x \in V \land P \in ℙ \land P ∥ (K - 1))$
24	1	numclwwlk5	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (x \in V \land P \in ℙ \land P ∥ (K - 1))) \to \|x ClWWalksNOn (G) P\| \mod P = 1$
25	19 23 24	syl2an2r	$⊢ (((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \land x \in V) \to \|x ClWWalksNOn (G) P\| \mod P = 1$
26	25	sumeq2dv	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} (\|x ClWWalksNOn (G) P\| \mod P) = \sum_{x \in V} 1$
27	26	oveq1d	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} (\|x ClWWalksNOn (G) P\| \mod P) \mod P = \sum_{x \in V} 1 \mod P$
28	18 27	eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} \|x ClWWalksNOn (G) P\| \mod P = \sum_{x \in V} 1 \mod P$
29		1cnd	$⊢ (P \in ℙ \land P ∥ (K - 1)) \to 1 \in ℂ$
30		fsumconst	$⊢ (V \in Fin \land 1 \in ℂ) \to \sum_{x \in V} 1 = \|V\| \cdot 1$
31	10 29 30	syl2an	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} 1 = \|V\| \cdot 1$
32		hashcl	$⊢ V \in Fin \to \|V\| \in ℕ_{0}$
33	32	nn0red	$⊢ V \in Fin \to \|V\| \in ℝ$
34		ax-1rid	$⊢ \|V\| \in ℝ \to \|V\| \cdot 1 = \|V\|$
35	33 34	syl	$⊢ V \in Fin \to \|V\| \cdot 1 = \|V\|$
36	35	3ad2ant3	$⊢ (G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \to \|V\| \cdot 1 = \|V\|$
37	36	adantr	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|V\| \cdot 1 = \|V\|$
38	31 37	eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} 1 = \|V\|$
39	38	oveq1d	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \sum_{x \in V} 1 \mod P = \|V\| \mod P$
40	8 28 39	3eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph \land V \in Fin) \land (P \in ℙ \land P ∥ (K - 1))) \to \|P ClWWalksN G\| \mod P = \|V\| \mod P$

Metamath Proof Explorer

Theorem numclwwlk6

Proof