Theorem wwlknlsw

Description: If a word represents a walk of a fixed length, then the last symbol of the word is the endvertex of the walk. (Contributed by AV, 8-Mar-2022)

	Ref	Expression
Assertion	wwlknlsw	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ‘ 𝑁 ) = ( lastS ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		wwlknbp1	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
2		lsw	⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
3	2	3ad2ant2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
4		oveq1	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
5	4	3ad2ant3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
6		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
7		pncan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
8	6 7	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
9	8	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
10	5 9	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
11	10	fveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ 𝑁 ) )
12	3 11	eqtr2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ‘ 𝑁 ) = ( lastS ‘ 𝑊 ) )
13	1 12	syl	⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑊 ‘ 𝑁 ) = ( lastS ‘ 𝑊 ) )