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 ⊢G∈USGraph∧W∈NClWWalksNG→W⁡N−1∈GNeighbVtxW⁡0

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢Edg⁡G=Edg⁡G
3 1 2 clwwlknp ⊢W∈NClWWalksNG→W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
4 lsw ⊢W∈WordVtx⁡G→lastS⁡W=W⁡W−1
5 fvoveq1 ⊢W=N→W⁡W−1=W⁡N−1
6 4 5 sylan9eq ⊢W∈WordVtx⁡G∧W=N→lastS⁡W=W⁡N−1
7 6 preq1d ⊢W∈WordVtx⁡G∧W=N→lastS⁡WW⁡0=W⁡N−1W⁡0
8 7 eleq1d ⊢W∈WordVtx⁡G∧W=N→lastS⁡WW⁡0∈Edg⁡G↔W⁡N−1W⁡0∈Edg⁡G
9 8 biimpd ⊢W∈WordVtx⁡G∧W=N→lastS⁡WW⁡0∈Edg⁡G→W⁡N−1W⁡0∈Edg⁡G
10 9 a1d ⊢W∈WordVtx⁡G∧W=N→∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G→lastS⁡WW⁡0∈Edg⁡G→W⁡N−1W⁡0∈Edg⁡G
11 10 3imp ⊢W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G→W⁡N−1W⁡0∈Edg⁡G
12 3 11 syl ⊢W∈NClWWalksNG→W⁡N−1W⁡0∈Edg⁡G
13 12 adantl ⊢G∈USGraph∧W∈NClWWalksNG→W⁡N−1W⁡0∈Edg⁡G
14 2 nbusgreledg ⊢G∈USGraph→W⁡N−1∈GNeighbVtxW⁡0↔W⁡N−1W⁡0∈Edg⁡G
15 14 adantr ⊢G∈USGraph∧W∈NClWWalksNG→W⁡N−1∈GNeighbVtxW⁡0↔W⁡N−1W⁡0∈Edg⁡G
16 13 15 mpbird ⊢G∈USGraph∧W∈NClWWalksNG→W⁡N−1∈GNeighbVtxW⁡0