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 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) )