# Metamath Proof Explorer

## Theorem wwlknllvtx

Description: If a word W represents a walk of a fixed length N , then the first and the last symbol of the word is a vertex. (Contributed by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlknllvtx.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
Assertion wwlknllvtx ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\left(0\right)\in {V}\wedge {W}\left({N}\right)\in {V}\right)$

### Proof

Step Hyp Ref Expression
1 wwlknllvtx.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wwlknbp1 ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({N}\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}+1\right)$
3 wwlknvtx ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \forall {x}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)$
4 0elfz ${⊢}{N}\in {ℕ}_{0}\to 0\in \left(0\dots {N}\right)$
5 fveq2 ${⊢}{x}=0\to {W}\left({x}\right)={W}\left(0\right)$
6 5 eleq1d ${⊢}{x}=0\to \left({W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)↔{W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\right)$
7 6 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {x}=0\right)\to \left({W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)↔{W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\right)$
8 4 7 rspcdv ${⊢}{N}\in {ℕ}_{0}\to \left(\forall {x}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)\to {W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\right)$
9 nn0fz0 ${⊢}{N}\in {ℕ}_{0}↔{N}\in \left(0\dots {N}\right)$
10 9 biimpi ${⊢}{N}\in {ℕ}_{0}\to {N}\in \left(0\dots {N}\right)$
11 fveq2 ${⊢}{x}={N}\to {W}\left({x}\right)={W}\left({N}\right)$
12 11 eleq1d ${⊢}{x}={N}\to \left({W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)↔{W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)$
13 12 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {x}={N}\right)\to \left({W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)↔{W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)$
14 10 13 rspcdv ${⊢}{N}\in {ℕ}_{0}\to \left(\forall {x}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)\to {W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)$
15 8 14 jcad ${⊢}{N}\in {ℕ}_{0}\to \left(\forall {x}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)\to \left({W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\wedge {W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)\right)$
16 15 3ad2ant1 ${⊢}\left({N}\in {ℕ}_{0}\wedge {W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}+1\right)\to \left(\forall {x}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{W}\left({x}\right)\in \mathrm{Vtx}\left({G}\right)\to \left({W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\wedge {W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)\right)$
17 2 3 16 sylc ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\wedge {W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)$
18 1 eleq2i ${⊢}{W}\left(0\right)\in {V}↔{W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)$
19 1 eleq2i ${⊢}{W}\left({N}\right)\in {V}↔{W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)$
20 18 19 anbi12i ${⊢}\left({W}\left(0\right)\in {V}\wedge {W}\left({N}\right)\in {V}\right)↔\left({W}\left(0\right)\in \mathrm{Vtx}\left({G}\right)\wedge {W}\left({N}\right)\in \mathrm{Vtx}\left({G}\right)\right)$
21 17 20 sylibr ${⊢}{W}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({W}\left(0\right)\in {V}\wedge {W}\left({N}\right)\in {V}\right)$