# Metamath Proof Explorer

## Theorem clwwlknlbonbgr1

Description: The last but one vertex in a closed walk is a neighbor of the first vertex of the closed walk. (Contributed by AV, 17-Feb-2022)

Ref Expression
Assertion clwwlknlbonbgr1 ${⊢}\left({G}\in \mathrm{USGraph}\wedge {W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to {W}\left({N}-1\right)\in \left({G}\mathrm{NeighbVtx}{W}\left(0\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{Edg}\left({G}\right)$
3 1 2 clwwlknp ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
4 lsw ${⊢}{W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \mathrm{lastS}\left({W}\right)={W}\left(\left|{W}\right|-1\right)$
5 fvoveq1 ${⊢}\left|{W}\right|={N}\to {W}\left(\left|{W}\right|-1\right)={W}\left({N}-1\right)$
6 4 5 sylan9eq ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to \mathrm{lastS}\left({W}\right)={W}\left({N}-1\right)$
7 6 preq1d ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}=\left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}$
8 7 eleq1d ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)↔\left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
9 8 biimpd ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
10 9 a1d ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\to \left(\forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \left(\left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\to \left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\right)$
11 10 3imp ${⊢}\left(\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge \forall {i}\in \left(0..^{N}-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in \mathrm{Edg}\left({G}\right)\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)\to \left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)$
12 3 11 syl ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\to \left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)$
13 12 adantl ${⊢}\left({G}\in \mathrm{USGraph}\wedge {W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to \left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)$
14 2 nbusgreledg ${⊢}{G}\in \mathrm{USGraph}\to \left({W}\left({N}-1\right)\in \left({G}\mathrm{NeighbVtx}{W}\left(0\right)\right)↔\left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
15 14 adantr ${⊢}\left({G}\in \mathrm{USGraph}\wedge {W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to \left({W}\left({N}-1\right)\in \left({G}\mathrm{NeighbVtx}{W}\left(0\right)\right)↔\left\{{W}\left({N}-1\right),{W}\left(0\right)\right\}\in \mathrm{Edg}\left({G}\right)\right)$
16 13 15 mpbird ${⊢}\left({G}\in \mathrm{USGraph}\wedge {W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\right)\to {W}\left({N}-1\right)\in \left({G}\mathrm{NeighbVtx}{W}\left(0\right)\right)$