numclwwlk1

Description: Statement 9 in Huneke p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since G is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0, but not for n=2, since F = (/) , but ( X C 2 ) , the set of closed walks with length 2 on X , see 2clwwlk2 , needs not be (/) in this case. This is because of the special definition of F and the usage of words to represent (closed) walks, and does not contradict Huneke's statement, which would read "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)", where f(0)=1 is the number of empty closed walks on v, see numclwlk1lem1 . If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 . This case, however, is not required to prove the friendship theorem. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 6-Mar-2022) (Proof shortened by AV, 31-Jul-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	$⊢ V = Vtx (G)$
	extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
Assertion	numclwwlk1	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X C N\| = K \|F\|$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
5	4	ad2antlr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to G \in USGraph$
6		simprl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to X \in V$
7		simprr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to N \in ℤ_{\geq 3}$
8	1 2 3	numclwwlk1lem2	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (X C N) \approx (F \times (G NeighbVtx X))$
9	5 6 7 8	syl3anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to (X C N) \approx (F \times (G NeighbVtx X))$
10		hasheni	$⊢ (X C N) \approx (F \times (G NeighbVtx X)) \to \|X C N\| = \|F \times (G NeighbVtx X)\|$
11	9 10	syl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X C N\| = \|F \times (G NeighbVtx X)\|$
12		eqid	$⊢ Vtx (G) = Vtx (G)$
13	12	clwwlknonfin	$⊢ Vtx (G) \in Fin \to X ClWWalksNOn (G) (N - 2) \in Fin$
14	1	eleq1i	$⊢ V \in Fin \leftrightarrow Vtx (G) \in Fin$
15	3	eleq1i	$⊢ F \in Fin \leftrightarrow X ClWWalksNOn (G) (N - 2) \in Fin$
16	13 14 15	3imtr4i	$⊢ V \in Fin \to F \in Fin$
17	16	adantr	$⊢ (V \in Fin \land G RegUSGraph K) \to F \in Fin$
18	17	adantr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to F \in Fin$
19	1	finrusgrfusgr	$⊢ (G RegUSGraph K \land V \in Fin) \to G \in FinUSGraph$
20	19	ancoms	$⊢ (V \in Fin \land G RegUSGraph K) \to G \in FinUSGraph$
21		fusgrfis	$⊢ G \in FinUSGraph \to Edg (G) \in Fin$
22	20 21	syl	$⊢ (V \in Fin \land G RegUSGraph K) \to Edg (G) \in Fin$
23	22	adantr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to Edg (G) \in Fin$
24		eqid	$⊢ Edg (G) = Edg (G)$
25	1 24	nbusgrfi	$⊢ (G \in USGraph \land Edg (G) \in Fin \land X \in V) \to G NeighbVtx X \in Fin$
26	5 23 6 25	syl3anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to G NeighbVtx X \in Fin$
27		hashxp	$⊢ (F \in Fin \land G NeighbVtx X \in Fin) \to \|F \times (G NeighbVtx X)\| = \|F\| \|G NeighbVtx X\|$
28	18 26 27	syl2anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F \times (G NeighbVtx X)\| = \|F\| \|G NeighbVtx X\|$
29	1	rusgrpropnb	$⊢ G RegUSGraph K \to (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall x \in V \|G NeighbVtx x\| = K)$
30		oveq2	$⊢ x = X \to G NeighbVtx x = G NeighbVtx X$
31	30	fveqeq2d	$⊢ x = X \to (\|G NeighbVtx x\| = K \leftrightarrow \|G NeighbVtx X\| = K)$
32	31	rspccv	$⊢ \forall x \in V \|G NeighbVtx x\| = K \to (X \in V \to \|G NeighbVtx X\| = K)$
33	32	3ad2ant3	$⊢ (G \in USGraph \land K \in ℕ_{0}^{*} \land \forall x \in V \|G NeighbVtx x\| = K) \to (X \in V \to \|G NeighbVtx X\| = K)$
34	29 33	syl	$⊢ G RegUSGraph K \to (X \in V \to \|G NeighbVtx X\| = K)$
35	34	adantl	$⊢ (V \in Fin \land G RegUSGraph K) \to (X \in V \to \|G NeighbVtx X\| = K)$
36	35	com12	$⊢ X \in V \to ((V \in Fin \land G RegUSGraph K) \to \|G NeighbVtx X\| = K)$
37	36	adantr	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to ((V \in Fin \land G RegUSGraph K) \to \|G NeighbVtx X\| = K)$
38	37	impcom	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|G NeighbVtx X\| = K$
39	38	oveq2d	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F\| \|G NeighbVtx X\| = \|F\| K$
40		hashcl	$⊢ F \in Fin \to \|F\| \in ℕ_{0}$
41		nn0cn	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℂ$
42	18 40 41	3syl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F\| \in ℂ$
43	20	adantr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to G \in FinUSGraph$
44		simplr	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to G RegUSGraph K$
45		ne0i	$⊢ X \in V \to V \neq \emptyset$
46	45	adantr	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to V \neq \emptyset$
47	46	adantl	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to V \neq \emptyset$
48	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
49	43 44 47 48	syl3anc	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to K \in ℕ_{0}$
50	49	nn0cnd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to K \in ℂ$
51	42 50	mulcomd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F\| K = K \|F\|$
52	39 51	eqtrd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|F\| \|G NeighbVtx X\| = K \|F\|$
53	11 28 52	3eqtrd	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X C N\| = K \|F\|$

Metamath Proof Explorer

Theorem numclwwlk1

Proof