Metamath Proof Explorer

Theorem wwlksnredwwlkn0

Description: For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (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 wwlksnredwwlkn0 
|- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )

Proof

Step Hyp Ref Expression
1 wwlksnredwwlkn.e 
 |-  E = ( Edg ` G )
2 1 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 ) ) )
3 2 imp 
 |-  ( ( 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 ) )
4 simpl 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W prefix ( N + 1 ) ) = y )
5 4 adantl 
 |-  ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( W prefix ( N + 1 ) ) = y )
6 fveq1 
 |-  ( y = ( W prefix ( N + 1 ) ) -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
7 6 eqcoms 
 |-  ( ( W prefix ( N + 1 ) ) = y -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
8 7 adantr 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( y ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 9 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 ) )
11 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
12 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
13 nn0re 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. RR )
14 lep1 
 |-  ( ( N + 1 ) e. RR -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
15 12 13 14 3syl 
 |-  ( N e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
16 peano2nn0 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
17 16 nn0zd 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. ZZ )
18 fznn 
 |-  ( ( ( N + 1 ) + 1 ) e. ZZ -> ( ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) ) )
19 12 17 18 3syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) ) )
20 11 15 19 mpbir2and 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) )
21 oveq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 1 ... ( # ` W ) ) = ( 1 ... ( ( N + 1 ) + 1 ) ) )
22 21 eleq2d 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` W ) ) <-> ( N + 1 ) e. ( 1 ... ( ( N + 1 ) + 1 ) ) ) )
23 20 22 imbitrrid 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
24 23 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
25 simpl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> W e. Word ( Vtx ` G ) )
26 24 25 jctild 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
27 26 3adant3 
 |-  ( ( 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 e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
28 10 27 syl 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
29 28 impcom 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
30 29 adantl 
 |-  ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
31 30 adantr 
 |-  ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
32 31 adantl 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
33 pfxfv0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
34 32 33 syl 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
35 simprll 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( W ` 0 ) = P )
36 8 34 35 3eqtrd 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) ) -> ( y ` 0 ) = P )
37 36 ex 
 |-  ( ( W prefix ( N + 1 ) ) = y -> ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( y ` 0 ) = P ) )
38 37 adantr 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( y ` 0 ) = P ) )
39 38 impcom 
 |-  ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( y ` 0 ) = P )
40 simpr 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> { ( lastS ` y ) , ( lastS ` W ) } e. E )
41 40 adantl 
 |-  ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> { ( lastS ` y ) , ( lastS ` W ) } e. E )
42 5 39 41 3jca 
 |-  ( ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) /\ ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) -> ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) )
43 42 ex 
 |-  ( ( ( ( W ` 0 ) = P /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) /\ y e. ( N WWalksN G ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
44 43 reximdva 
 |-  ( ( ( W ` 0 ) = P /\ ( 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 ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
45 44 ex 
 |-  ( ( W ` 0 ) = P -> ( ( 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 ) -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) )
46 45 com13 
 |-  ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) ) )
47 3 46 mpcom 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P -> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
48 29 33 syl 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
49 48 eqcomd 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
50 49 adantl 
 |-  ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
51 fveq1 
 |-  ( ( W prefix ( N + 1 ) ) = y -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) )
52 51 adantr 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) )
53 52 adantr 
 |-  ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( y ` 0 ) )
54 simpr 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( y ` 0 ) = P )
55 54 adantr 
 |-  ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( y ` 0 ) = P )
56 50 53 55 3eqtrd 
 |-  ( ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) /\ ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) ) -> ( W ` 0 ) = P )
57 56 ex 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = P ) )
58 57 3adant3 
 |-  ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( W ` 0 ) = P ) )
59 58 com12 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W ` 0 ) = P ) )
60 59 rexlimdvw 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) -> ( W ` 0 ) = P ) )
61 47 60 impbid 
 |-  ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( W prefix ( N + 1 ) ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )