Metamath Proof Explorer

Theorem wwlknlsw

Description: If a word represents a walk of a fixed length, then the last symbol of the word is the endvertex of the walk. (Contributed by AV, 8-Mar-2022)

Ref Expression
Assertion wwlknlsw 
|- ( W e. ( N WWalksN G ) -> ( W ` N ) = ( lastS ` W ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
2 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
3 2 3ad2ant2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
4 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
5 4 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
6 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
7 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
8 6 7 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
9 8 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( N + 1 ) - 1 ) = N )
10 5 9 eqtrd 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) - 1 ) = N )
11 10 fveq2d 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` N ) )
12 3 11 eqtr2d 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( W ` N ) = ( lastS ` W ) )
13 1 12 syl 
 |-  ( W e. ( N WWalksN G ) -> ( W ` N ) = ( lastS ` W ) )