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 ∈ N ClWWalksN G → W ⁡ N − 1 ∈ G NeighbVtx W ⁡ 0

Proof

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