Metamath Proof Explorer

Theorem wwlksnredwwlkn

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 26-Oct-2022)

Ref Expression
Hypothesis wwlksnredwwlkn.e 
|- E = ( Edg ` G )
Assertion wwlksnredwwlkn 
|- ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e 
 |-  E = ( Edg ` G )
2 eqidd 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 1 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 simprl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> W e. Word ( Vtx ` G ) )
6 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
7 peano2nn0 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
8 6 7 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
9 id 
 |-  ( N e. NN0 -> N e. NN0 )
10 nn0p1nn 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN )
11 6 10 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) e. NN )
12 nn0re 
 |-  ( N e. NN0 -> N e. RR )
13 id 
 |-  ( N e. RR -> N e. RR )
14 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
15 peano2re 
 |-  ( ( N + 1 ) e. RR -> ( ( N + 1 ) + 1 ) e. RR )
16 14 15 syl 
 |-  ( N e. RR -> ( ( N + 1 ) + 1 ) e. RR )
17 13 14 16 3jca 
 |-  ( N e. RR -> ( N e. RR /\ ( N + 1 ) e. RR /\ ( ( N + 1 ) + 1 ) e. RR ) )
18 12 17 syl 
 |-  ( N e. NN0 -> ( N e. RR /\ ( N + 1 ) e. RR /\ ( ( N + 1 ) + 1 ) e. RR ) )
19 12 ltp1d 
 |-  ( N e. NN0 -> N < ( N + 1 ) )
20 nn0re 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. RR )
21 6 20 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
22 21 ltp1d 
 |-  ( N e. NN0 -> ( N + 1 ) < ( ( N + 1 ) + 1 ) )
23 lttr 
 |-  ( ( N e. RR /\ ( N + 1 ) e. RR /\ ( ( N + 1 ) + 1 ) e. RR ) -> ( ( N < ( N + 1 ) /\ ( N + 1 ) < ( ( N + 1 ) + 1 ) ) -> N < ( ( N + 1 ) + 1 ) ) )
24 23 imp 
 |-  ( ( ( N e. RR /\ ( N + 1 ) e. RR /\ ( ( N + 1 ) + 1 ) e. RR ) /\ ( N < ( N + 1 ) /\ ( N + 1 ) < ( ( N + 1 ) + 1 ) ) ) -> N < ( ( N + 1 ) + 1 ) )
25 18 19 22 24 syl12anc 
 |-  ( N e. NN0 -> N < ( ( N + 1 ) + 1 ) )
26 elfzo0 
 |-  ( N e. ( 0 ..^ ( ( N + 1 ) + 1 ) ) <-> ( N e. NN0 /\ ( ( N + 1 ) + 1 ) e. NN /\ N < ( ( N + 1 ) + 1 ) ) )
27 9 11 25 26 syl3anbrc 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( ( N + 1 ) + 1 ) ) )
28 fz0add1fz1 
 |-  ( ( ( ( N + 1 ) + 1 ) e. NN0 /\ N e. ( 0 ..^ ( ( N + 1 ) + 1 ) ) ) -> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) )
29 8 27 28 syl2anc 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) )
30 29 adantr 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) )
31 oveq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( ( N + 1 ) + 1 ) ) )
32 31 eleq2d 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) )
33 32 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) )
34 33 adantl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) )
35 30 34 mpbird 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) )
36 5 35 jca 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
37 36 3adantr3 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
38 pfxfvlsw 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix ( N + 1 ) ) ) = ( W ` ( ( N + 1 ) - 1 ) ) )
39 37 38 syl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> ( lastS ` ( W prefix ( N + 1 ) ) ) = ( W ` ( ( N + 1 ) - 1 ) ) )
40 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
41 40 3ad2ant1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
42 41 adantl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
43 39 42 preq12d 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } = { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( # ` W ) - 1 ) ) } )
44 oveq1 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( # ` W ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
45 44 3ad2ant2 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( ( # ` W ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
46 45 adantl 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> ( ( # ` W ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
47 46 fveq2d 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) )
48 47 preq2d 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( # ` W ) - 1 ) ) } = { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) } )
49 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
50 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
51 49 50 pncand 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
52 51 fveq2d 
 |-  ( N e. NN0 -> ( W ` ( ( N + 1 ) - 1 ) ) = ( W ` N ) )
53 6 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
54 53 50 pncand 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
55 54 fveq2d 
 |-  ( N e. NN0 -> ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) = ( W ` ( N + 1 ) ) )
56 52 55 preq12d 
 |-  ( N e. NN0 -> { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
57 56 adantr 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( ( N + 1 ) + 1 ) - 1 ) ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
58 48 57 eqtrd 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( # ` W ) - 1 ) ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
59 fveq2 
 |-  ( i = N -> ( W ` i ) = ( W ` N ) )
60 fvoveq1 
 |-  ( i = N -> ( W ` ( i + 1 ) ) = ( W ` ( N + 1 ) ) )
61 59 60 preq12d 
 |-  ( i = N -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` N ) , ( W ` ( N + 1 ) ) } )
62 61 eleq1d 
 |-  ( i = N -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E <-> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
63 62 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 ) )
64 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
65 63 64 syl11 
 |-  ( A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E -> ( N e. NN0 -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
66 65 3ad2ant3 
 |-  ( ( 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 -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E ) )
67 66 impcom 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( W ` N ) , ( W ` ( N + 1 ) ) } e. E )
68 58 67 eqeltrd 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( W ` ( ( N + 1 ) - 1 ) ) , ( W ` ( ( # ` W ) - 1 ) ) } e. E )
69 43 68 eqeltrd 
 |-  ( ( N e. NN0 /\ ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E )
70 4 69 sylan2 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E )
71 wwlksnred 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) )
72 71 imp 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) )
73 eqeq2 
 |-  ( y = ( W prefix ( N + 1 ) ) -> ( ( W prefix ( N + 1 ) ) = y <-> ( W prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) ) )
74 fveq2 
 |-  ( y = ( W prefix ( N + 1 ) ) -> ( lastS ` y ) = ( lastS ` ( W prefix ( N + 1 ) ) ) )
75 74 preq1d 
 |-  ( y = ( W prefix ( N + 1 ) ) -> { ( lastS ` y ) , ( lastS ` W ) } = { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } )
76 75 eleq1d 
 |-  ( y = ( W prefix ( N + 1 ) ) -> ( { ( lastS ` y ) , ( lastS ` W ) } e. E <-> { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) )
77 73 76 anbi12d 
 |-  ( y = ( W prefix ( N + 1 ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) <-> ( ( W prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) /\ { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) ) )
78 77 adantl 
 |-  ( ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) /\ y = ( W prefix ( N + 1 ) ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) <-> ( ( W prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) /\ { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) ) )
79 72 78 rspcedv 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( ( W prefix ( N + 1 ) ) = ( W prefix ( N + 1 ) ) /\ { ( lastS ` ( W prefix ( N + 1 ) ) ) , ( lastS ` W ) } e. E ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
80 2 70 79 mp2and 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) )
81 80 ex 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )