Metamath Proof Explorer

Theorem rusgrnumwlkg

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. This theorem corresponds to statement 11 in Huneke p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular." This theorem even holds for n=0: then the walk consists of only one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 5-Aug-2022)

Ref Expression
Hypothesis rusgrnumwwlkg.v 
|- V = ( Vtx ` G )
Assertion rusgrnumwlkg 
|- ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } ) = ( K ^ N ) )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkg.v 
 |-  V = ( Vtx ` G )
2 ovex 
 |-  ( N WWalksN G ) e. _V
3 2 rabex 
 |-  { p e. ( N WWalksN G ) | ( p ` 0 ) = P } e. _V
4 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
5 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
6 4 5 syl 
 |-  ( G RegUSGraph K -> G e. USPGraph )
7 simp3 
 |-  ( ( V e. Fin /\ P e. V /\ N e. NN0 ) -> N e. NN0 )
8 wlksnwwlknvbij 
 |-  ( ( G e. USPGraph /\ N e. NN0 ) -> E. f f : { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } -1-1-onto-> { p e. ( N WWalksN G ) | ( p ` 0 ) = P } )
9 6 7 8 syl2an 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> E. f f : { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } -1-1-onto-> { p e. ( N WWalksN G ) | ( p ` 0 ) = P } )
10 f1oexbi 
 |-  ( E. g g : { p e. ( N WWalksN G ) | ( p ` 0 ) = P } -1-1-onto-> { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } <-> E. f f : { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } -1-1-onto-> { p e. ( N WWalksN G ) | ( p ` 0 ) = P } )
11 9 10 sylibr 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> E. g g : { p e. ( N WWalksN G ) | ( p ` 0 ) = P } -1-1-onto-> { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } )
12 hasheqf1oi 
 |-  ( { p e. ( N WWalksN G ) | ( p ` 0 ) = P } e. _V -> ( E. g g : { p e. ( N WWalksN G ) | ( p ` 0 ) = P } -1-1-onto-> { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } -> ( # ` { p e. ( N WWalksN G ) | ( p ` 0 ) = P } ) = ( # ` { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } ) ) )
13 3 11 12 mpsyl 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { p e. ( N WWalksN G ) | ( p ` 0 ) = P } ) = ( # ` { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } ) )
14 1 rusgrnumwwlkg 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { p e. ( N WWalksN G ) | ( p ` 0 ) = P } ) = ( K ^ N ) )
15 13 14 eqtr3d 
 |-  ( ( G RegUSGraph K /\ ( V e. Fin /\ P e. V /\ N e. NN0 ) ) -> ( # ` { w e. ( Walks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = P ) } ) = ( K ^ N ) )