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 ⊢ W ∈ N WWalksN G → W ⁡ N = lastS ⁡ W

Proof

Step Hyp Ref Expression
1 wwlknbp1 ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
2 lsw ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ W − 1
3 2 3ad2ant2 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → lastS ⁡ W = W ⁡ W − 1
4 oveq1 ⊢ W = N + 1 → W − 1 = N + 1 - 1
5 4 3ad2ant3 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → W − 1 = N + 1 - 1
6 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
7 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
8 6 7 syl ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
9 8 3ad2ant1 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → N + 1 - 1 = N
10 5 9 eqtrd ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → W − 1 = N
11 10 fveq2d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → W ⁡ W − 1 = W ⁡ N
12 3 11 eqtr2d ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → W ⁡ N = lastS ⁡ W
13 1 12 syl ⊢ W ∈ N WWalksN G → W ⁡ N = lastS ⁡ W