Theorem rusgrnumwwlkb1

Description: Induction base 1 for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 28-Jul-2018) (Revised by AV, 7-May-2021)

	Ref	Expression
Hypotheses	rusgrnumwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	rusgrnumwwlk.l	⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
Assertion	rusgrnumwwlkb1	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 1 ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		rusgrnumwwlk.l	⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
3		simpr	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → 𝑃 ∈ 𝑉 )
4		1nn0	⊢ 1 ∈ ℕ0
5	1 2	rusgrnumwwlklem	⊢ ( ( 𝑃 ∈ 𝑉 ∧ 1 ∈ ℕ0 ) → ( 𝑃 𝐿 1 ) = ( ♯ ‘ { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
6	3 4 5	sylancl	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 1 ) = ( ♯ ‘ { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
7	1	rusgrnumwwlkl1	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = 𝐾 )
8	6 7	eqtrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 1 ) = 𝐾 )