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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	rusgrnumwwlkg	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlkg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		3simpc	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
3	2	adantl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
4		eqid	⊢ ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
5	1 4	rusgrnumwwlklem	⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
6	3 5	syl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑃 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
7	1 4	rusgrnumwwlk	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑃 ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) ) 𝑁 ) = ( 𝐾 ↑ 𝑁 ) )
8	6 7	eqtr3d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) )