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 \in (N WWalksN G) \to W (N) = lastS (W)$

Proof

Step	Hyp	Ref	Expression
1		wwlknbp1	$⊢ W \in (N WWalksN G) \to (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)$
2		lsw	$⊢ W \in Word Vtx (G) \to lastS (W) = W (\|W\| - 1)$
3	2	3ad2ant2	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to lastS (W) = W (\|W\| - 1)$
4		oveq1	$⊢ \|W\| = N + 1 \to \|W\| - 1 = N + 1 - 1$
5	4	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| - 1 = N + 1 - 1$
6		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
7		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
8	6 7	syl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
9	8	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N + 1 - 1 = N$
10	5 9	eqtrd	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| - 1 = N$
11	10	fveq2d	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to W (\|W\| - 1) = W (N)$
12	3 11	eqtr2d	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to W (N) = lastS (W)$
13	1 12	syl	$⊢ W \in (N WWalksN G) \to W (N) = lastS (W)$