Metamath Proof Explorer

Theorem rusgrnumwwlkg

Description: In a K-regular graph, the number of walks (as words) of a fixed length N from a fixed vertex is K to the power of N . Closed form of rusgrnumwwlk . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 7-May-2021)

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

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlkg.v	$⊢ V = Vtx (G)$
2		3simpc	$⊢ (V \in Fin \land P \in V \land N \in ℕ_{0}) \to (P \in V \land N \in ℕ_{0})$
3	2	adantl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to (P \in V \land N \in ℕ_{0})$
4		eqid	$⊢ (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|) = (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|)$
5	1 4	rusgrnumwwlklem	$⊢ (P \in V \land N \in ℕ_{0}) \to P (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|) N = \|\{w \in (N WWalksN G) \| w (0) = P\}\|$
6	3 5	syl	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to P (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|) N = \|\{w \in (N WWalksN G) \| w (0) = P\}\|$
7	1 4	rusgrnumwwlk	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to P (v \in V, n \in ℕ_{0} ⟼ \|\{w \in (n WWalksN G) \| w (0) = v\}\|) N = K^{N}$
8	6 7	eqtr3d	$⊢ (G RegUSGraph K \land (V \in Fin \land P \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| w (0) = P\}\| = K^{N}$