Metamath Proof Explorer

Theorem redwlk

Description: A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion redwlk 
|- ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 iswlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
5 wrdred1 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) )
6 5 a1i 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F e. Word dom ( iEdg ` G ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) ) )
7 3 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
8 redwlklem 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ 1 <_ ( # ` F ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) )
9 8 3exp 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( 1 <_ ( # ` F ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) ) ) )
10 7 9 syl 
 |-  ( F ( Walks ` G ) P -> ( 1 <_ ( # ` F ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) ) ) )
11 10 imp 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) ) )
12 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
13 wrdred1hash 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )
14 7 13 sylan 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )
15 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
16 fzossrbm1 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
17 15 16 syl 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
18 ssralv 
 |-  ( ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
19 17 18 syl 
 |-  ( ( # ` F ) e. NN0 -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
20 17 sselda 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> k e. ( 0 ..^ ( # ` F ) ) )
21 20 fvresd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( P ` k ) )
22 21 eqcomd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( P ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) )
23 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
24 simpr 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) )
25 15 adantr 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( # ` F ) e. ZZ )
26 1zzd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> 1 e. ZZ )
27 fzoaddel2 
 |-  ( ( k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) /\ ( # ` F ) e. ZZ /\ 1 e. ZZ ) -> ( k + 1 ) e. ( 1 ..^ ( # ` F ) ) )
28 24 25 26 27 syl3anc 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( k + 1 ) e. ( 1 ..^ ( # ` F ) ) )
29 23 28 sselid 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( k + 1 ) e. ( 0 ..^ ( # ` F ) ) )
30 29 fvresd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
31 30 eqcomd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( P ` ( k + 1 ) ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) )
32 22 31 eqeq12d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( P ` k ) = ( P ` ( k + 1 ) ) <-> ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) ) )
33 fvres 
 |-  ( k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) = ( F ` k ) )
34 33 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) = ( F ` k ) )
35 34 eqcomd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( F ` k ) = ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) )
36 35 fveq2d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) )
37 22 sneqd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> { ( P ` k ) } = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } )
38 36 37 eqeq12d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } <-> ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } ) )
39 22 31 preq12d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } )
40 39 36 sseq12d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) <-> { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) )
41 32 38 40 ifpbi123d 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
42 41 biimpd 
 |-  ( ( ( # ` F ) e. NN0 /\ k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
43 42 ralimdva 
 |-  ( ( # ` F ) e. NN0 -> ( A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
44 19 43 syld 
 |-  ( ( # ` F ) e. NN0 -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
45 44 adantr 
 |-  ( ( ( # ` F ) e. NN0 /\ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
46 oveq2 
 |-  ( ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) -> ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) = ( 0 ..^ ( ( # ` F ) - 1 ) ) )
47 46 eqcomd 
 |-  ( ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) = ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) )
48 47 raleqdv 
 |-  ( ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) -> ( A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) <-> A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
49 48 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) -> ( A. k e. ( 0 ..^ ( ( # ` F ) - 1 ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) <-> A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
50 45 49 sylibd 
 |-  ( ( ( # ` F ) e. NN0 /\ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
51 12 14 50 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
52 6 11 51 3anim123d 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) /\ ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) ) )
53 52 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) /\ ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) )
54 id 
 |-  ( G e. _V -> G e. _V )
55 resexg 
 |-  ( F e. _V -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. _V )
56 resexg 
 |-  ( P e. _V -> ( P |` ( 0 ..^ ( # ` F ) ) ) e. _V )
57 2 3 iswlk 
 |-  ( ( G e. _V /\ ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. _V /\ ( P |` ( 0 ..^ ( # ` F ) ) ) e. _V ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) <-> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) /\ ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) ) )
58 57 bicomd 
 |-  ( ( G e. _V /\ ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. _V /\ ( P |` ( 0 ..^ ( # ` F ) ) ) e. _V ) -> ( ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) /\ ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) <-> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) )
59 54 55 56 58 syl3an 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word dom ( iEdg ` G ) /\ ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) if- ( ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) = ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) = { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) } , { ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` k ) , ( ( P |` ( 0 ..^ ( # ` F ) ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ` k ) ) ) ) <-> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) )
60 53 59 imbitrid 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) )
61 60 expcomd 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) ) )
62 4 61 sylbid 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P -> ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) ) )
63 1 62 mpcom 
 |-  ( F ( Walks ` G ) P -> ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) ) )
64 63 anabsi5 
 |-  ( ( F ( Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ( Walks ` G ) ( P |` ( 0 ..^ ( # ` F ) ) ) )