Metamath Proof Explorer


Theorem wwlknvtx

Description: The symbols of a word W representing a walk of a fixed length N are vertices. (Contributed by AV, 16-Mar-2022)

Ref Expression
Assertion wwlknvtx ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
2 simp2 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
3 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
4 fzval3 ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
5 3 4 syl ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
6 5 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
7 6 eleq2d ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
8 7 biimpa ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
9 oveq2 ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
10 9 eleq2d ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
11 10 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
12 11 adantr ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
13 8 12 mpbird ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 wrdsymbcl ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
15 2 13 14 syl2an2r ( ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑊𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
16 15 ralrimiva ( ( 𝑁 ∈ ℕ0𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )
17 1 16 syl ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑊𝑖 ) ∈ ( Vtx ‘ 𝐺 ) )