This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wwlknllvtx ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 wwlknllvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknbp1 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
3 wwlknvtx ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) )
4 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
5 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 0 ) )
6 5 eleq1d ⊢ ( 𝑥 = 0 → ( ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) ↔ ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
7 6 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 = 0 ) → ( ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) ↔ ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
8 4 7 rspcdv ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) → ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
9 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
10 9 biimpi ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... 𝑁 ) )
11 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 𝑁 ) )
12 11 eleq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) ↔ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) )
13 12 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 = 𝑁 ) → ( ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) ↔ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) )
14 10 13 rspcdv ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) → ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) )
15 8 14 jcad ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) ) )
16 15 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ∀ 𝑥 ∈ ( 0 ... 𝑁 ) ( 𝑊 ‘ 𝑥 ) ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) ) )
17 2 3 16 sylc ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) )
18 1 eleq2i ⊢ ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ↔ ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
19 1 eleq2i ⊢ ( ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ↔ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) )
20 18 19 anbi12i ⊢ ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) ↔ ( ( 𝑊 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 ‘ 𝑁 ) ∈ ( Vtx ‘ 𝐺 ) ) )
21 17 20 sylibr ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) )