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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion rusgrnumwlkg ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } ) = ( 𝐾𝑁 ) )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlkg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 ovex ( 𝑁 WWalksN 𝐺 ) ∈ V
3 2 rabex { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ∈ V
4 rusgrusgr ( 𝐺 RegUSGraph 𝐾𝐺 ∈ USGraph )
5 usgruspgr ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
6 4 5 syl ( 𝐺 RegUSGraph 𝐾𝐺 ∈ USPGraph )
7 simp3 ( ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
8 wlksnwwlknvbij ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } )
9 6 7 8 syl2an ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } )
10 f1oexbi ( ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } ↔ ∃ 𝑓 𝑓 : { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } –1-1-onto→ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } )
11 9 10 sylibr ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } )
12 hasheqf1oi ( { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ∈ V → ( ∃ 𝑔 𝑔 : { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } –1-1-onto→ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } ) ) )
13 3 11 12 mpsyl ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } ) )
14 1 rusgrnumwwlkg ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑝 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑝 ‘ 0 ) = 𝑃 } ) = ( 𝐾𝑁 ) )
15 13 14 eqtr3d ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( Walks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st𝑤 ) ) = 𝑁 ∧ ( ( 2nd𝑤 ) ‘ 0 ) = 𝑃 ) } ) = ( 𝐾𝑁 ) )