Metamath Proof Explorer

Theorem 2clwwlklem

Description: Lemma for clwwnonrepclwwnon and extwwlkfab . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 10-May-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Assertion 2clwwlklem 
|- ( ( W e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ` 0 ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 clwwlknwrd 
 |-  ( W e. ( N ClWWalksN G ) -> W e. Word ( Vtx ` G ) )
3 ige3m2fz 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 1 ... N ) )
4 3 adantl 
 |-  ( ( W e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. ( 1 ... N ) )
5 clwwlknlen 
 |-  ( W e. ( N ClWWalksN G ) -> ( # ` W ) = N )
6 5 oveq2d 
 |-  ( W e. ( N ClWWalksN G ) -> ( 1 ... ( # ` W ) ) = ( 1 ... N ) )
7 6 eleq2d 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( N - 2 ) e. ( 1 ... ( # ` W ) ) <-> ( N - 2 ) e. ( 1 ... N ) ) )
8 7 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) e. ( 1 ... ( # ` W ) ) <-> ( N - 2 ) e. ( 1 ... N ) ) )
9 4 8 mpbird 
 |-  ( ( W e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. ( 1 ... ( # ` W ) ) )
10 pfxfv0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N - 2 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix ( N - 2 ) ) ` 0 ) = ( W ` 0 ) )
11 2 9 10 syl2an2r 
 |-  ( ( W e. ( N ClWWalksN G ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ` 0 ) = ( W ` 0 ) )