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 e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlkg.v	|- V = ( Vtx ` G )
2		3simpc	|- ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> ( P e. V /\ N e. NN0 ) )
3	2	adantl	|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( P e. V /\ N e. NN0 ) )
4		eqid	|- ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) ) = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
5	1 4	rusgrnumwwlklem	|- ( ( P e. V /\ N e. NN0 ) -> ( P ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) ) N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
6	3 5	syl	|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( P ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) ) N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
7	1 4	rusgrnumwwlk	|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( P ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) ) N ) = ( K ^ N ) )
8	6 7	eqtr3d	|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( K ^ N ) )