rusgrnumwlkg

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. This theorem corresponds to statement 11 in Huneke p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular." This theorem even holds for n=0: then the walk consists of only one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 5-Aug-2022)

		Ref	Expression
	Hypothesis	rusgrnumwwlkg.v	$⊢ V = Vtx (G)$
	Assertion	rusgrnumwlkg	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \|\{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\}\| = K^{N}$

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlkg.v	$⊢ V = Vtx (G)$
2		ovex	$⊢ N WWalksN G \in V$
3	2	rabex	$⊢ \{p \in (N WWalksN G) \| p (0) = P\} \in V$
4		rusgrusgr	$⊢ G RegUSGraph K \to G \in USGraph$
5		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
6	4 5	syl	$⊢ G RegUSGraph K \to G \in USHGraph$
7		simp3	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to N \in ℕ_{0}$
8		wlksnwwlknvbij	$⊢ (G \in USHGraph \land N \in ℕ_{0}) \to \exists f f : \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\} \underset{1-1 onto}{⟶} \{p \in (N WWalksN G) \| p (0) = P\}$
9	6 7 8	syl2an	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \exists f f : \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\} \underset{1-1 onto}{⟶} \{p \in (N WWalksN G) \| p (0) = P\}$
10		f1oexbi	$⊢ \exists g g : \{p \in (N WWalksN G) \| p (0) = P\} \underset{1-1 onto}{⟶} \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\} \leftrightarrow \exists f f : \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\} \underset{1-1 onto}{⟶} \{p \in (N WWalksN G) \| p (0) = P\}$
11	9 10	sylibr	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \exists g g : \{p \in (N WWalksN G) \| p (0) = P\} \underset{1-1 onto}{⟶} \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\}$
12		hasheqf1oi	$⊢ \{p \in (N WWalksN G) \| p (0) = P\} \in V \to (\exists g g : \{p \in (N WWalksN G) \| p (0) = P\} \underset{1-1 onto}{⟶} \{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\} \to \|\{p \in (N WWalksN G) \| p (0) = P\}\| = \|\{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\}\|)$
13	3 11 12	mpsyl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \|\{p \in (N WWalksN G) \| p (0) = P\}\| = \|\{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\}\|$
14	1	rusgrnumwwlkg	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \|\{p \in (N WWalksN G) \| p (0) = P\}\| = K^{N}$
15	13 14	eqtr3d	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \|\{w \in Walks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = P)\}\| = K^{N}$

Metamath Proof Explorer

Theorem rusgrnumwlkg

Proof