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 = Vtx ⁡ G
Assertion wwlknllvtx ⊢ W ∈ N WWalksN G → W ⁡ 0 ∈ V ∧ W ⁡ N ∈ V

Proof

Step Hyp Ref Expression
1 wwlknllvtx.v ⊢ V = Vtx ⁡ G
2 wwlknbp1 ⊢ W ∈ N WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1
3 wwlknvtx ⊢ W ∈ N WWalksN G → ∀ x ∈ 0 … N W ⁡ x ∈ Vtx ⁡ G
4 0elfz ⊢ N ∈ ℕ 0 → 0 ∈ 0 … N
5 fveq2 ⊢ x = 0 → W ⁡ x = W ⁡ 0
6 5 eleq1d ⊢ x = 0 → W ⁡ x ∈ Vtx ⁡ G ↔ W ⁡ 0 ∈ Vtx ⁡ G
7 6 adantl ⊢ N ∈ ℕ 0 ∧ x = 0 → W ⁡ x ∈ Vtx ⁡ G ↔ W ⁡ 0 ∈ Vtx ⁡ G
8 4 7 rspcdv ⊢ N ∈ ℕ 0 → ∀ x ∈ 0 … N W ⁡ x ∈ Vtx ⁡ G → W ⁡ 0 ∈ Vtx ⁡ G
9 nn0fz0 ⊢ N ∈ ℕ 0 ↔ N ∈ 0 … N
10 9 biimpi ⊢ N ∈ ℕ 0 → N ∈ 0 … N
11 fveq2 ⊢ x = N → W ⁡ x = W ⁡ N
12 11 eleq1d ⊢ x = N → W ⁡ x ∈ Vtx ⁡ G ↔ W ⁡ N ∈ Vtx ⁡ G
13 12 adantl ⊢ N ∈ ℕ 0 ∧ x = N → W ⁡ x ∈ Vtx ⁡ G ↔ W ⁡ N ∈ Vtx ⁡ G
14 10 13 rspcdv ⊢ N ∈ ℕ 0 → ∀ x ∈ 0 … N W ⁡ x ∈ Vtx ⁡ G → W ⁡ N ∈ Vtx ⁡ G
15 8 14 jcad ⊢ N ∈ ℕ 0 → ∀ x ∈ 0 … N W ⁡ x ∈ Vtx ⁡ G → W ⁡ 0 ∈ Vtx ⁡ G ∧ W ⁡ N ∈ Vtx ⁡ G
16 15 3ad2ant1 ⊢ N ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = N + 1 → ∀ x ∈ 0 … N W ⁡ x ∈ Vtx ⁡ G → W ⁡ 0 ∈ Vtx ⁡ G ∧ W ⁡ N ∈ Vtx ⁡ G
17 2 3 16 sylc ⊢ W ∈ N WWalksN G → W ⁡ 0 ∈ Vtx ⁡ G ∧ W ⁡ N ∈ Vtx ⁡ G
18 1 eleq2i ⊢ W ⁡ 0 ∈ V ↔ W ⁡ 0 ∈ Vtx ⁡ G
19 1 eleq2i ⊢ W ⁡ N ∈ V ↔ W ⁡ N ∈ Vtx ⁡ G
20 18 19 anbi12i ⊢ W ⁡ 0 ∈ V ∧ W ⁡ N ∈ V ↔ W ⁡ 0 ∈ Vtx ⁡ G ∧ W ⁡ N ∈ Vtx ⁡ G
21 17 20 sylibr ⊢ W ∈ N WWalksN G → W ⁡ 0 ∈ V ∧ W ⁡ N ∈ V