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=VtxG
Assertion rusgrnumwlkg GRegUSGraphKVFinPVN0wWalksG|1stw=N2ndw0=P=KN

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkg.v V=VtxG
2 ovex NWWalksNGV
3 2 rabex pNWWalksNG|p0=PV
4 rusgrusgr GRegUSGraphKGUSGraph
5 usgruspgr GUSGraphGUSHGraph
6 4 5 syl GRegUSGraphKGUSHGraph
7 simp3 VFinPVN0N0
8 wlksnwwlknvbij GUSHGraphN0ff:wWalksG|1stw=N2ndw0=P1-1 ontopNWWalksNG|p0=P
9 6 7 8 syl2an GRegUSGraphKVFinPVN0ff:wWalksG|1stw=N2ndw0=P1-1 ontopNWWalksNG|p0=P
10 f1oexbi gg:pNWWalksNG|p0=P1-1 ontowWalksG|1stw=N2ndw0=Pff:wWalksG|1stw=N2ndw0=P1-1 ontopNWWalksNG|p0=P
11 9 10 sylibr GRegUSGraphKVFinPVN0gg:pNWWalksNG|p0=P1-1 ontowWalksG|1stw=N2ndw0=P
12 hasheqf1oi pNWWalksNG|p0=PVgg:pNWWalksNG|p0=P1-1 ontowWalksG|1stw=N2ndw0=PpNWWalksNG|p0=P=wWalksG|1stw=N2ndw0=P
13 3 11 12 mpsyl GRegUSGraphKVFinPVN0pNWWalksNG|p0=P=wWalksG|1stw=N2ndw0=P
14 1 rusgrnumwwlkg GRegUSGraphKVFinPVN0pNWWalksNG|p0=P=KN
15 13 14 eqtr3d GRegUSGraphKVFinPVN0wWalksG|1stw=N2ndw0=P=KN