Metamath Proof Explorer


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 ‘ 𝑊 ) )