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∈NWWalksNG→W⁡0∈V∧W⁡N∈V

Proof

Step Hyp Ref Expression
1 wwlknllvtx.v ⊢V=Vtx⁡G
2 wwlknbp1 ⊢W∈NWWalksNG→N∈ℕ0∧W∈WordVtx⁡G∧W=N+1
3 wwlknvtx ⊢W∈NWWalksNG→∀x∈0…NW⁡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…NW⁡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…NW⁡x∈Vtx⁡G→W⁡N∈Vtx⁡G
15 8 14 jcad ⊢N∈ℕ0→∀x∈0…NW⁡x∈Vtx⁡G→W⁡0∈Vtx⁡G∧W⁡N∈Vtx⁡G
16 15 3ad2ant1 ⊢N∈ℕ0∧W∈WordVtx⁡G∧W=N+1→∀x∈0…NW⁡x∈Vtx⁡G→W⁡0∈Vtx⁡G∧W⁡N∈Vtx⁡G
17 2 3 16 sylc ⊢W∈NWWalksNG→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∈NWWalksNG→W⁡0∈V∧W⁡N∈V