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 ) = 𝑃 ) } ) = ( 𝐾 ↑ 𝑁 ) )