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 | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| rusgrnumwwlk.l | ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) | ||
| Assertion | rusgrnumwwlk | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rusgrnumwwlk.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | rusgrnumwwlk.l | ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) | |
| 3 | oveq2 | ⊢ ( 𝑥 = 0 → ( 𝑃 𝐿 𝑥 ) = ( 𝑃 𝐿 0 ) ) | |
| 4 | oveq2 | ⊢ ( 𝑥 = 0 → ( 𝐾 ↑ 𝑥 ) = ( 𝐾 ↑ 0 ) ) | |
| 5 | 3 4 | eqeq12d | ⊢ ( 𝑥 = 0 → ( ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ↔ ( 𝑃 𝐿 0 ) = ( 𝐾 ↑ 0 ) ) ) |
| 6 | 5 | imbi2d | ⊢ ( 𝑥 = 0 → ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ) ↔ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 0 ) = ( 𝐾 ↑ 0 ) ) ) ) |
| 7 | oveq2 | ⊢ ( 𝑥 = 𝑦 → ( 𝑃 𝐿 𝑥 ) = ( 𝑃 𝐿 𝑦 ) ) | |
| 8 | oveq2 | ⊢ ( 𝑥 = 𝑦 → ( 𝐾 ↑ 𝑥 ) = ( 𝐾 ↑ 𝑦 ) ) | |
| 9 | 7 8 | eqeq12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ↔ ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) ) ) |
| 10 | 9 | imbi2d | ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ) ↔ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) ) ) ) |
| 11 | oveq2 | ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝑃 𝐿 ( 𝑦 + 1 ) ) ) | |
| 12 | oveq2 | ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐾 ↑ 𝑥 ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) | |
| 13 | 11 12 | eqeq12d | ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ↔ ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) |
| 14 | 13 | imbi2d | ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ) ↔ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) ) |
| 15 | oveq2 | ⊢ ( 𝑥 = 𝑁 → ( 𝑃 𝐿 𝑥 ) = ( 𝑃 𝐿 𝑁 ) ) | |
| 16 | oveq2 | ⊢ ( 𝑥 = 𝑁 → ( 𝐾 ↑ 𝑥 ) = ( 𝐾 ↑ 𝑁 ) ) | |
| 17 | 15 16 | eqeq12d | ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ↔ ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) |
| 18 | 17 | imbi2d | ⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝐾 ↑ 𝑥 ) ) ↔ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) ) |
| 19 | rusgrusgr | ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph ) | |
| 20 | usgruspgr | ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph ) | |
| 21 | 19 20 | syl | ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph ) |
| 22 | simpr | ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) → 𝑃 ∈ 𝑉 ) | |
| 23 | 1 2 | rusgrnumwwlkb0 | ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 0 ) = 1 ) |
| 24 | 21 22 23 | syl2anr | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 0 ) = 1 ) |
| 25 | simpl | ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) → 𝑉 ∈ Fin ) | |
| 26 | 25 19 | anim12ci | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
| 27 | 1 | isfusgr | ⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
| 28 | 26 27 | sylibr | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph ) |
| 29 | simpr | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 RegUSGraph 𝐾 ) | |
| 30 | ne0i | ⊢ ( 𝑃 ∈ 𝑉 → 𝑉 ≠ ∅ ) | |
| 31 | 30 | ad2antlr | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝑉 ≠ ∅ ) |
| 32 | 1 | frusgrnn0 | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 ) |
| 33 | 32 | nn0cnd | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℂ ) |
| 34 | 28 29 31 33 | syl3anc | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐾 ∈ ℂ ) |
| 35 | 34 | exp0d | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 ↑ 0 ) = 1 ) |
| 36 | 24 35 | eqtr4d | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 0 ) = ( 𝐾 ↑ 0 ) ) |
| 37 | simpl | ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ) | |
| 38 | 37 | anim1i | ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝑦 ∈ ℕ0 ) ) |
| 39 | df-3an | ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0 ) ↔ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝑦 ∈ ℕ0 ) ) | |
| 40 | 38 39 | sylibr | ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0 ) ) |
| 41 | 1 2 | rusgrnumwwlks | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) → ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) |
| 42 | 29 40 41 | syl2an2r | ⊢ ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) → ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) |
| 43 | 42 | expcom | ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) → ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) ) |
| 44 | 43 | a2d | ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑦 ) = ( 𝐾 ↑ 𝑦 ) ) → ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 ( 𝑦 + 1 ) ) = ( 𝐾 ↑ ( 𝑦 + 1 ) ) ) ) ) |
| 45 | 6 10 14 18 36 44 | nn0ind | ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) |
| 46 | 45 | expd | ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) → ( 𝐺 RegUSGraph 𝐾 → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) ) |
| 47 | 46 | com12 | ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ) → ( 𝑁 ∈ ℕ0 → ( 𝐺 RegUSGraph 𝐾 → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) ) |
| 48 | 47 | 3impia | ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐺 RegUSGraph 𝐾 → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) ) |
| 49 | 48 | impcom | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ) |