Metamath Proof Explorer

Theorem pfxwlk

Description: A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023)

Ref Expression
Assertion pfxwlk 
|- ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
3 2 adantr 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> F e. Word dom ( iEdg ` G ) )
4 pfxcl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( F prefix L ) e. Word dom ( iEdg ` G ) )
5 3 4 syl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) e. Word dom ( iEdg ` G ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
8 7 adantr 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
9 elfzuz3 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` L ) )
10 fzss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` L ) -> ( 0 ... L ) C_ ( 0 ... ( # ` F ) ) )
11 9 10 syl 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> ( 0 ... L ) C_ ( 0 ... ( # ` F ) ) )
12 11 adantl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... L ) C_ ( 0 ... ( # ` F ) ) )
13 8 12 fssresd 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P |` ( 0 ... L ) ) : ( 0 ... L ) --> ( Vtx ` G ) )
14 pfxlen 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix L ) ) = L )
15 2 14 sylan 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix L ) ) = L )
16 15 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... ( # ` ( F prefix L ) ) ) = ( 0 ... L ) )
17 16 feq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( P |` ( 0 ... L ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) <-> ( P |` ( 0 ... L ) ) : ( 0 ... L ) --> ( Vtx ` G ) ) )
18 13 17 mpbird 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P |` ( 0 ... L ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) )
19 6 wlkpwrd 
 |-  ( F ( Walks ` G ) P -> P e. Word ( Vtx ` G ) )
20 fzp1elp1 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> ( L + 1 ) e. ( 0 ... ( ( # ` F ) + 1 ) ) )
21 20 adantl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L + 1 ) e. ( 0 ... ( ( # ` F ) + 1 ) ) )
22 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
23 22 oveq2d 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` P ) ) = ( 0 ... ( ( # ` F ) + 1 ) ) )
24 23 adantr 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... ( # ` P ) ) = ( 0 ... ( ( # ` F ) + 1 ) ) )
25 21 24 eleqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( L + 1 ) e. ( 0 ... ( # ` P ) ) )
26 pfxres 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( L + 1 ) e. ( 0 ... ( # ` P ) ) ) -> ( P prefix ( L + 1 ) ) = ( P |` ( 0 ..^ ( L + 1 ) ) ) )
27 19 25 26 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P prefix ( L + 1 ) ) = ( P |` ( 0 ..^ ( L + 1 ) ) ) )
28 elfzelz 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> L e. ZZ )
29 fzval3 
 |-  ( L e. ZZ -> ( 0 ... L ) = ( 0 ..^ ( L + 1 ) ) )
30 28 29 syl 
 |-  ( L e. ( 0 ... ( # ` F ) ) -> ( 0 ... L ) = ( 0 ..^ ( L + 1 ) ) )
31 30 adantl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ... L ) = ( 0 ..^ ( L + 1 ) ) )
32 31 reseq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P |` ( 0 ... L ) ) = ( P |` ( 0 ..^ ( L + 1 ) ) ) )
33 27 32 eqtr4d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P prefix ( L + 1 ) ) = ( P |` ( 0 ... L ) ) )
34 33 feq1d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( P prefix ( L + 1 ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) <-> ( P |` ( 0 ... L ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) ) )
35 18 34 mpbird 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( P prefix ( L + 1 ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) )
36 6 1 wlkprop 
 |-  ( F ( Walks ` G ) P -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) ) )
37 36 simp3d 
 |-  ( F ( Walks ` G ) P -> A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) )
38 37 adantr 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) )
39 38 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) )
40 15 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ ( # ` ( F prefix L ) ) ) = ( 0 ..^ L ) )
41 40 eleq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) <-> k e. ( 0 ..^ L ) ) )
42 33 fveq1d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P |` ( 0 ... L ) ) ` k ) )
43 42 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P |` ( 0 ... L ) ) ` k ) )
44 fzossfz 
 |-  ( 0 ..^ L ) C_ ( 0 ... L )
45 44 a1i 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ L ) C_ ( 0 ... L ) )
46 45 sselda 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> k e. ( 0 ... L ) )
47 46 fvresd 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( P |` ( 0 ... L ) ) ` k ) = ( P ` k ) )
48 43 47 eqtr2d 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) )
49 33 fveq1d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) = ( ( P |` ( 0 ... L ) ) ` ( k + 1 ) ) )
50 49 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) = ( ( P |` ( 0 ... L ) ) ` ( k + 1 ) ) )
51 fzofzp1 
 |-  ( k e. ( 0 ..^ L ) -> ( k + 1 ) e. ( 0 ... L ) )
52 51 adantl 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( k + 1 ) e. ( 0 ... L ) )
53 52 fvresd 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( P |` ( 0 ... L ) ) ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
54 50 53 eqtr2d 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) )
55 48 54 jca 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) )
56 55 ex 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( k e. ( 0 ..^ L ) -> ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) ) )
57 41 56 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) -> ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) ) )
58 57 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) )
59 3 ancli 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ F e. Word dom ( iEdg ` G ) ) )
60 simpr 
 |-  ( ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ F e. Word dom ( iEdg ` G ) ) /\ k e. ( 0 ..^ L ) ) -> k e. ( 0 ..^ L ) )
61 60 fvresd 
 |-  ( ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ F e. Word dom ( iEdg ` G ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( F |` ( 0 ..^ L ) ) ` k ) = ( F ` k ) )
62 61 fveq2d 
 |-  ( ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ F e. Word dom ( iEdg ` G ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) = ( ( iEdg ` G ) ` ( F ` k ) ) )
63 59 62 sylan 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) = ( ( iEdg ` G ) ` ( F ` k ) ) )
64 63 eqcomd 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ L ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) )
65 64 ex 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( k e. ( 0 ..^ L ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) ) )
66 41 65 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) ) )
67 66 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) )
68 simplr 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> L e. ( 0 ... ( # ` F ) ) )
69 pfxres 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) = ( F |` ( 0 ..^ L ) ) )
70 3 68 69 syl2an2r 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( F prefix L ) = ( F |` ( 0 ..^ L ) ) )
71 70 fveq1d 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( F prefix L ) ` k ) = ( ( F |` ( 0 ..^ L ) ) ` k ) )
72 71 fveq2d 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = ( ( iEdg ` G ) ` ( ( F |` ( 0 ..^ L ) ) ` k ) ) )
73 67 72 eqtr4d 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) )
74 58 73 jca 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) )
75 9 adantl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` L ) )
76 15 fveq2d 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ZZ>= ` ( # ` ( F prefix L ) ) ) = ( ZZ>= ` L ) )
77 75 76 eleqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` ( # ` ( F prefix L ) ) ) )
78 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( # ` ( F prefix L ) ) ) -> ( 0 ..^ ( # ` ( F prefix L ) ) ) C_ ( 0 ..^ ( # ` F ) ) )
79 77 78 syl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ ( # ` ( F prefix L ) ) ) C_ ( 0 ..^ ( # ` F ) ) )
80 79 sselda 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> k e. ( 0 ..^ ( # ` F ) ) )
81 wkslem1 
 |-  ( x = k -> ( if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
82 81 rspcv 
 |-  ( k e. ( 0 ..^ ( # ` F ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
83 80 82 syl 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
84 eqeq12 
 |-  ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) -> ( ( P ` k ) = ( P ` ( k + 1 ) ) <-> ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) )
85 84 adantr 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( ( P ` k ) = ( P ` ( k + 1 ) ) <-> ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) )
86 simpr 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) )
87 sneq 
 |-  ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) -> { ( P ` k ) } = { ( ( P prefix ( L + 1 ) ) ` k ) } )
88 87 adantr 
 |-  ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) -> { ( P ` k ) } = { ( ( P prefix ( L + 1 ) ) ` k ) } )
89 88 adantr 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> { ( P ` k ) } = { ( ( P prefix ( L + 1 ) ) ` k ) } )
90 86 89 eqeq12d 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } <-> ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } ) )
91 preq12 
 |-  ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } )
92 91 adantr 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } )
93 92 86 sseq12d 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) <-> { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) )
94 85 90 93 ifpbi123d 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) <-> if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) ) )
95 94 biimpd 
 |-  ( ( ( ( P ` k ) = ( ( P prefix ( L + 1 ) ) ` k ) /\ ( P ` ( k + 1 ) ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) ) /\ ( ( iEdg ` G ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) -> if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) ) )
96 74 83 95 sylsyld 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` x ) = ( P ` ( x + 1 ) ) , ( ( iEdg ` G ) ` ( F ` x ) ) = { ( P ` x ) } , { ( P ` x ) , ( P ` ( x + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` x ) ) ) -> if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) ) )
97 39 96 mpd 
 |-  ( ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) /\ k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) ) -> if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) )
98 97 ralrimiva 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> A. k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) )
99 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
100 99 simp1d 
 |-  ( F ( Walks ` G ) P -> G e. _V )
101 100 adantr 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> G e. _V )
102 6 1 iswlkg 
 |-  ( G e. _V -> ( ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) <-> ( ( F prefix L ) e. Word dom ( iEdg ` G ) /\ ( P prefix ( L + 1 ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) ) ) )
103 101 102 syl 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) <-> ( ( F prefix L ) e. Word dom ( iEdg ` G ) /\ ( P prefix ( L + 1 ) ) : ( 0 ... ( # ` ( F prefix L ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( F prefix L ) ) ) if- ( ( ( P prefix ( L + 1 ) ) ` k ) = ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) = { ( ( P prefix ( L + 1 ) ) ` k ) } , { ( ( P prefix ( L + 1 ) ) ` k ) , ( ( P prefix ( L + 1 ) ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( F prefix L ) ` k ) ) ) ) ) )
104 5 35 98 103 mpbir3and 
 |-  ( ( F ( Walks ` G ) P /\ L e. ( 0 ... ( # ` F ) ) ) -> ( F prefix L ) ( Walks ` G ) ( P prefix ( L + 1 ) ) )