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 e. ( N WWalksN G ) -> ( ( W ` 0 ) e. V /\ ( W ` N ) e. V ) )

Proof

Step Hyp Ref Expression
1 wwlknllvtx.v 
 |-  V = ( Vtx ` G )
2 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
3 wwlknvtx 
 |-  ( W e. ( N WWalksN G ) -> A. x e. ( 0 ... N ) ( W ` x ) e. ( Vtx ` G ) )
4 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
5 fveq2 
 |-  ( x = 0 -> ( W ` x ) = ( W ` 0 ) )
6 5 eleq1d 
 |-  ( x = 0 -> ( ( W ` x ) e. ( Vtx ` G ) <-> ( W ` 0 ) e. ( Vtx ` G ) ) )
7 6 adantl 
 |-  ( ( N e. NN0 /\ x = 0 ) -> ( ( W ` x ) e. ( Vtx ` G ) <-> ( W ` 0 ) e. ( Vtx ` G ) ) )
8 4 7 rspcdv 
 |-  ( N e. NN0 -> ( A. x e. ( 0 ... N ) ( W ` x ) e. ( Vtx ` G ) -> ( W ` 0 ) e. ( Vtx ` G ) ) )
9 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
10 9 biimpi 
 |-  ( N e. NN0 -> N e. ( 0 ... N ) )
11 fveq2 
 |-  ( x = N -> ( W ` x ) = ( W ` N ) )
12 11 eleq1d 
 |-  ( x = N -> ( ( W ` x ) e. ( Vtx ` G ) <-> ( W ` N ) e. ( Vtx ` G ) ) )
13 12 adantl 
 |-  ( ( N e. NN0 /\ x = N ) -> ( ( W ` x ) e. ( Vtx ` G ) <-> ( W ` N ) e. ( Vtx ` G ) ) )
14 10 13 rspcdv 
 |-  ( N e. NN0 -> ( A. x e. ( 0 ... N ) ( W ` x ) e. ( Vtx ` G ) -> ( W ` N ) e. ( Vtx ` G ) ) )
15 8 14 jcad 
 |-  ( N e. NN0 -> ( A. x e. ( 0 ... N ) ( W ` x ) e. ( Vtx ` G ) -> ( ( W ` 0 ) e. ( Vtx ` G ) /\ ( W ` N ) e. ( Vtx ` G ) ) ) )
16 15 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( A. x e. ( 0 ... N ) ( W ` x ) e. ( Vtx ` G ) -> ( ( W ` 0 ) e. ( Vtx ` G ) /\ ( W ` N ) e. ( Vtx ` G ) ) ) )
17 2 3 16 sylc 
 |-  ( W e. ( N WWalksN G ) -> ( ( W ` 0 ) e. ( Vtx ` G ) /\ ( W ` N ) e. ( Vtx ` G ) ) )
18 1 eleq2i 
 |-  ( ( W ` 0 ) e. V <-> ( W ` 0 ) e. ( Vtx ` G ) )
19 1 eleq2i 
 |-  ( ( W ` N ) e. V <-> ( W ` N ) e. ( Vtx ` G ) )
20 18 19 anbi12i 
 |-  ( ( ( W ` 0 ) e. V /\ ( W ` N ) e. V ) <-> ( ( W ` 0 ) e. ( Vtx ` G ) /\ ( W ` N ) e. ( Vtx ` G ) ) )
21 17 20 sylibr 
 |-  ( W e. ( N WWalksN G ) -> ( ( W ` 0 ) e. V /\ ( W ` N ) e. V ) )