numclwwlk3

Description: Statement 12 in Huneke p. 2: "Thus f(n) = (k - 1)f(n - 2) + k^(n-2)." - the number of the closed walks v(0) ... v(n-2) v(n-1) v(n) is the sum of the number of the closed walks v(0) ... v(n-2) v(n-1) v(n) with v(n-2) = v(n) (see numclwwlk1 ) and with v(n-2) =/= v(n) (see numclwwlk2 ): f(n) = kf(n-2) + k^(n-2) - f(n-2) = (k-1)f(n-2) + k^(n-2). (Contributed by Alexander van der Vekens, 26-Aug-2018) (Revised by AV, 6-Mar-2022)

		Ref	Expression
	Hypothesis	numclwwlk3.v	$⊢ V = Vtx (G)$
	Assertion	numclwwlk3	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) N\| = (K - 1) \|X ClWWalksNOn (G) (N - 2)\| + K^{N - 2}$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3.v	$⊢ V = Vtx (G)$
2		simpl	$⊢ (G RegUSGraph K \land G \in FriendGraph) \to G RegUSGraph K$
3		simp1	$⊢ (V \in Fin \land X \in V \land N \in ℤ_{\geq 3}) \to V \in Fin$
4	1	finrusgrfusgr	$⊢ (G RegUSGraph K \land V \in Fin) \to G \in FinUSGraph$
5	2 3 4	syl2an	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to G \in FinUSGraph$
6		simpr2	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to X \in V$
7		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
8	7	3ad2ant3	$⊢ (V \in Fin \land X \in V \land N \in ℤ_{\geq 3}) \to N \in ℤ_{\geq 2}$
9	8	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to N \in ℤ_{\geq 2}$
10		eqid	$⊢ (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
11		eqid	$⊢ (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\}) = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
12	10 11	numclwwlk3lem2	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \|X ClWWalksNOn (G) N\| = \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\}) N\| + \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\|$
13	5 6 9 12	syl21anc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) N\| = \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\}) N\| + \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\|$
14		eqid	$⊢ (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\}) = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
15	1 14 11	numclwwlk2	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\}) N\| = K^{N - 2} - \|X ClWWalksNOn (G) (N - 2)\|$
16	2 3	anim12ci	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to (V \in Fin \land G RegUSGraph K)$
17		3simpc	$⊢ (V \in Fin \land X \in V \land N \in ℤ_{\geq 3}) \to (X \in V \land N \in ℤ_{\geq 3})$
18	17	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to (X \in V \land N \in ℤ_{\geq 3})$
19		eqid	$⊢ X ClWWalksNOn (G) (N - 2) = X ClWWalksNOn (G) (N - 2)$
20	1 10 19	numclwwlk1	$⊢ ((V \in Fin \land G RegUSGraph K) \land (X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = K \|X ClWWalksNOn (G) (N - 2)\|$
21	16 18 20	syl2anc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = K \|X ClWWalksNOn (G) (N - 2)\|$
22	15 21	oveq12d	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\}) N\| + \|X (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\}) N\| = K^{N - 2} - \|X ClWWalksNOn (G) (N - 2)\| + K \|X ClWWalksNOn (G) (N - 2)\|$
23		simpll	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to G RegUSGraph K$
24		ne0i	$⊢ X \in V \to V \neq \emptyset$
25	24	3ad2ant2	$⊢ (V \in Fin \land X \in V \land N \in ℤ_{\geq 3}) \to V \neq \emptyset$
26	25	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to V \neq \emptyset$
27	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
28	5 23 26 27	syl3anc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to K \in ℕ_{0}$
29	28	nn0cnd	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to K \in ℂ$
30		uz3m2nn	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ$
31	30	3anim3i	$⊢ (V \in Fin \land X \in V \land N \in ℤ_{\geq 3}) \to (V \in Fin \land X \in V \land N - 2 \in ℕ)$
32	31	adantl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to (V \in Fin \land X \in V \land N - 2 \in ℕ)$
33	1	clwwlknonfin	$⊢ V \in Fin \to X ClWWalksNOn (G) (N - 2) \in Fin$
34	33	3ad2ant1	$⊢ (V \in Fin \land X \in V \land N - 2 \in ℕ) \to X ClWWalksNOn (G) (N - 2) \in Fin$
35		hashcl	$⊢ X ClWWalksNOn (G) (N - 2) \in Fin \to \|X ClWWalksNOn (G) (N - 2)\| \in ℕ_{0}$
36	35	nn0cnd	$⊢ X ClWWalksNOn (G) (N - 2) \in Fin \to \|X ClWWalksNOn (G) (N - 2)\| \in ℂ$
37	32 34 36	3syl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) (N - 2)\| \in ℂ$
38		numclwwlk3lem1	$⊢ (K \in ℂ \land \|X ClWWalksNOn (G) (N - 2)\| \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} - \|X ClWWalksNOn (G) (N - 2)\| + K \|X ClWWalksNOn (G) (N - 2)\| = (K - 1) \|X ClWWalksNOn (G) (N - 2)\| + K^{N - 2}$
39	29 37 9 38	syl3anc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to K^{N - 2} - \|X ClWWalksNOn (G) (N - 2)\| + K \|X ClWWalksNOn (G) (N - 2)\| = (K - 1) \|X ClWWalksNOn (G) (N - 2)\| + K^{N - 2}$
40	13 22 39	3eqtrd	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \in Fin \land X \in V \land N \in ℤ_{\geq 3})) \to \|X ClWWalksNOn (G) N\| = (K - 1) \|X ClWWalksNOn (G) (N - 2)\| + K^{N - 2}$

Metamath Proof Explorer

Theorem numclwwlk3

Proof