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