Metamath Proof Explorer

Theorem wwlksnextproplem2

Description: Lemma 2 for wwlksnextprop . (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses wwlksnextprop.x 
|- X = ( ( N + 1 ) WWalksN G )
wwlksnextprop.e 
|- E = ( Edg ` G )
Assertion wwlksnextproplem2 
|- ( ( W e. X /\ N e. NN0 ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x 
 |-  X = ( ( N + 1 ) WWalksN G )
2 wwlksnextprop.e 
 |-  E = ( Edg ` G )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 2 wwlknp 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
5 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
6 5 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> N e. ( 0 ..^ ( N + 1 ) ) )
7 fveq2 
 |-  ( i = N -> ( W ` i ) = ( W ` N ) )
8 fvoveq1 
 |-  ( i = N -> ( W ` ( i + 1 ) ) = ( W ` ( N + 1 ) ) )
9 7 8 preq12d 
 |-  ( i = N -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
10 9 eleq1d 
 |-  ( i = N -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
11 10 rspcv 
 |-  ( N e. ( 0 ..^ ( N + 1 ) ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
12 6 11 syl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
13 12 imp 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E )
14 simpll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> W e. Word ( Vtx ` G ) )
15 1zzd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> 1 e. ZZ )
16 lencl 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) e. NN0 )
17 16 nn0zd 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) e. ZZ )
18 17 ad2antrr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( # ` W ) e. ZZ )
19 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
20 19 nn0zd 
 |-  ( N e. NN0 -> ( N + 1 ) e. ZZ )
21 20 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) e. ZZ )
22 15 18 21 3jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( 1 e. ZZ /\ ( # ` W ) e. ZZ /\ ( N + 1 ) e. ZZ ) )
23 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
24 1red 
 |-  ( N e. NN0 -> 1 e. RR )
25 nn0re 
 |-  ( N e. NN0 -> N e. RR )
26 24 25 addge02d 
 |-  ( N e. NN0 -> ( 0 <_ N <-> 1 <_ ( N + 1 ) ) )
27 23 26 mpbid 
 |-  ( N e. NN0 -> 1 <_ ( N + 1 ) )
28 27 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> 1 <_ ( N + 1 ) )
29 19 nn0red 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
30 29 lep1d 
 |-  ( N e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
31 breq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) <_ ( # ` W ) <-> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
32 30 31 syl5ibrcom 
 |-  ( N e. NN0 -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N + 1 ) <_ ( # ` W ) ) )
33 32 a1i 
 |-  ( ( # ` W ) e. NN0 -> ( N e. NN0 -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N + 1 ) <_ ( # ` W ) ) ) )
34 33 com23 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) <_ ( # ` W ) ) ) )
35 16 34 syl 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) <_ ( # ` W ) ) ) )
36 35 imp31 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( # ` W ) )
37 28 36 jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( 1 <_ ( N + 1 ) /\ ( N + 1 ) <_ ( # ` W ) ) )
38 elfz2 
 |-  ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( ( 1 e. ZZ /\ ( # ` W ) e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( 1 <_ ( N + 1 ) /\ ( N + 1 ) <_ ( # ` W ) ) ) )
39 22 37 38 sylanbrc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) )
40 pfxfvlsw 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix ( N + 1 ) ) ) = ( W ` ( ( N + 1 ) - 1 ) ) )
41 14 39 40 syl2anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( lastS ` ( W prefix ( N + 1 ) ) ) = ( W ` ( ( N + 1 ) - 1 ) ) )
42 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
43 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
44 42 43 pncand 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
45 44 fveq2d 
 |-  ( N e. NN0 -> ( W ` ( ( N + 1 ) - 1 ) ) = ( W ` N ) )
46 45 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W ` ( ( N + 1 ) - 1 ) ) = ( W ` N ) )
47 41 46 eqtrd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( lastS ` ( W prefix ( N + 1 ) ) ) = ( W ` N ) )
48 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
49 48 ad2antrr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
50 fvoveq1 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) )
51 50 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) )
52 19 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
53 52 43 pncand 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
54 53 fveq2d 
 |-  ( N e. NN0 -> ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) = ( W ` ( N + 1 ) ) )
55 51 54 sylan9eq 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( N + 1 ) ) )
56 49 55 eqtrd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( lastS ` W ) = ( W ` ( N + 1 ) ) )
57 47 56 preq12d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
58 57 eleq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E <-> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
59 58 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E <-> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
60 13 59 mpbird 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E )
61 60 exp31 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) ) )
62 61 com23 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> ( N e. NN0 -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) ) )
63 62 3impia 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( N e. NN0 -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) )
64 4 63 syl 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) )
65 64 1 eleq2s 
 |-  ( W e. X -> ( N e. NN0 -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) )
66 65 imp 
 |-  ( ( W e. X /\ N e. NN0 ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E )