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 ∧ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = P = K N

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkg.v ⊢ V = Vtx ⁡ G
2 3simpc ⊢ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → P ∈ V ∧ N ∈ ℕ 0
3 2 adantl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → P ∈ V ∧ N ∈ ℕ 0
4 eqid ⊢ v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v = v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v
5 1 4 rusgrnumwwlklem ⊢ P ∈ V ∧ N ∈ ℕ 0 → P v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v N = w ∈ N WWalksN G | w ⁡ 0 = P
6 3 5 syl ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → P v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v N = w ∈ N WWalksN G | w ⁡ 0 = P
7 1 4 rusgrnumwwlk ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → P v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v N = K N
8 6 7 eqtr3d ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ P ∈ V ∧ N ∈ ℕ 0 → w ∈ N WWalksN G | w ⁡ 0 = P = K N