This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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