rusgrnumwwlk

Description: In a K-regular graph, the number of walks of a fixed length N from a fixed vertex is K to the power of N . By definition, ( N WWalksN G ) is the set of walks (as words) with length N , and ( P L N ) is the number of walks with length N starting at the vertex P . Because of the K-regularity, a walk can be continued in K different ways at the end vertex of the walk, and this repeated N times.

This theorem even holds for N = 0 : in this case, the walk consists of only one vertex P , so the number of walks of length N = 0 starting with P is ( K ^ 0 ) = 1 . (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	$⊢ V = Vtx (G)$
	rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
Assertion	rusgrnumwwlk	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to P L N = K^{N}$

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	$⊢ V = Vtx (G)$
2		rusgrnumwwlk.l	$⊢ L = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
3		oveq2	$⊢ x = 0 \to P L x = P L 0$
4		oveq2	$⊢ x = 0 \to K^{x} = K^{0}$
5	3 4	eqeq12d	$⊢ x = 0 \to (P L x = K^{x} \leftrightarrow P L 0 = K^{0})$
6	5	imbi2d	$⊢ x = 0 \to ((((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L x = K^{x}) \leftrightarrow (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L 0 = K^{0}))$
7		oveq2	$⊢ x = y \to P L x = P L y$
8		oveq2	$⊢ x = y \to K^{x} = K^{y}$
9	7 8	eqeq12d	$⊢ x = y \to (P L x = K^{x} \leftrightarrow P L y = K^{y})$
10	9	imbi2d	$⊢ x = y \to ((((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L x = K^{x}) \leftrightarrow (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L y = K^{y}))$
11		oveq2	$⊢ x = y + 1 \to P L x = P L (y + 1)$
12		oveq2	$⊢ x = y + 1 \to K^{x} = K^{y + 1}$
13	11 12	eqeq12d	$⊢ x = y + 1 \to (P L x = K^{x} \leftrightarrow P L (y + 1) = K^{y + 1})$
14	13	imbi2d	$⊢ x = y + 1 \to ((((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L x = K^{x}) \leftrightarrow (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L (y + 1) = K^{y + 1}))$
15		oveq2	$⊢ x = N \to P L x = P L N$
16		oveq2	$⊢ x = N \to K^{x} = K^{N}$
17	15 16	eqeq12d	$⊢ x = N \to (P L x = K^{x} \leftrightarrow P L N = K^{N})$
18	17	imbi2d	$⊢ x = N \to ((((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L x = K^{x}) \leftrightarrow (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L N = K^{N}))$
19		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
20		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
21	19 20	syl	$⊢ G RegUSGraph K \to G \in USHGraph$
22		simpr	$⊢ (V \in Fin \land P \in V) \to P \in V$
23	1 2	rusgrnumwwlkb0	$⊢ (G \in USHGraph \land P \in V) \to P L 0 = 1$
24	21 22 23	syl2anr	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L 0 = 1$
25		simpl	$⊢ (V \in Fin \land P \in V) \to V \in Fin$
26	25 19	anim12ci	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to (G \in USGraph \land V \in Fin)$
27	1	isfusgr	$⊢ G \in FinUSGraph \leftrightarrow (G \in USGraph \land V \in Fin)$
28	26 27	sylibr	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to G \in FinUSGraph$
29		simpr	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to G RegUSGraph K$
30		ne0i	$⊢ P \in V \to V \neq \emptyset$
31	30	ad2antlr	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to V \neq \emptyset$
32	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
33	32	nn0cnd	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℂ$
34	28 29 31 33	syl3anc	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to K \in ℂ$
35	34	exp0d	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to K^{0} = 1$
36	24 35	eqtr4d	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L 0 = K^{0}$
37		simpl	$⊢ ((V \in Fin \land P \in V) \land G RegUSGraph K) \to (V \in Fin \land P \in V)$
38	37	anim1i	$⊢ (((V \in Fin \land P \in V) \land G RegUSGraph K) \land y \in ℕ_{0}) \to ((V \in Fin \land P \in V) \land y \in ℕ_{0})$
39		df-3an	$⊢ (V \in Fin \land P \in V \land y \in ℕ_{0}) \leftrightarrow ((V \in Fin \land P \in V) \land y \in ℕ_{0})$
40	38 39	sylibr	$⊢ (((V \in Fin \land P \in V) \land G RegUSGraph K) \land y \in ℕ_{0}) \to (V \in Fin \land P \in V \land y \in ℕ_{0})$
41	1 2	rusgrnumwwlks	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land y \in ℕ_{0})) \to (P L y = K^{y} \to P L (y + 1) = K^{y + 1})$
42	29 40 41	syl2an2r	$⊢ (((V \in Fin \land P \in V) \land G RegUSGraph K) \land y \in ℕ_{0}) \to (P L y = K^{y} \to P L (y + 1) = K^{y + 1})$
43	42	expcom	$⊢ y \in ℕ_{0} \to (((V \in Fin \land P \in V) \land G RegUSGraph K) \to (P L y = K^{y} \to P L (y + 1) = K^{y + 1}))$
44	43	a2d	$⊢ y \in ℕ_{0} \to ((((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L y = K^{y}) \to (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L (y + 1) = K^{y + 1}))$
45	6 10 14 18 36 44	nn0ind	$⊢ N \in ℕ_{0} \to (((V \in Fin \land P \in V) \land G RegUSGraph K) \to P L N = K^{N})$
46	45	expd	$⊢ N \in ℕ_{0} \to ((V \in Fin \land P \in V) \to (G RegUSGraph K \to P L N = K^{N}))$
47	46	com12	$⊢ (V \in Fin \land P \in V) \to (N \in ℕ_{0} \to (G RegUSGraph K \to P L N = K^{N}))$
48	47	3impia	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to (G RegUSGraph K \to P L N = K^{N})$
49	48	impcom	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to P L N = K^{N}$

Metamath Proof Explorer

Theorem rusgrnumwwlk

Proof