Metamath Proof Explorer

Theorem revwlk

Description: The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023)

Ref Expression
Assertion revwlk 
|- ( F ( Walks ` G ) P -> ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) )

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 revcl 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( reverse ` F ) e. Word dom ( iEdg ` G ) )
4 2 3 syl 
 |-  ( F ( Walks ` G ) P -> ( reverse ` F ) e. Word dom ( iEdg ` G ) )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 5 wlkpwrd 
 |-  ( F ( Walks ` G ) P -> P e. Word ( Vtx ` G ) )
7 revcl 
 |-  ( P e. Word ( Vtx ` G ) -> ( reverse ` P ) e. Word ( Vtx ` G ) )
8 wrdf 
 |-  ( ( reverse ` P ) e. Word ( Vtx ` G ) -> ( reverse ` P ) : ( 0 ..^ ( # ` ( reverse ` P ) ) ) --> ( Vtx ` G ) )
9 6 7 8 3syl 
 |-  ( F ( Walks ` G ) P -> ( reverse ` P ) : ( 0 ..^ ( # ` ( reverse ` P ) ) ) --> ( Vtx ` G ) )
10 revlen 
 |-  ( F e. Word dom ( iEdg ` G ) -> ( # ` ( reverse ` F ) ) = ( # ` F ) )
11 2 10 syl 
 |-  ( F ( Walks ` G ) P -> ( # ` ( reverse ` F ) ) = ( # ` F ) )
12 11 oveq2d 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` ( reverse ` F ) ) ) = ( 0 ... ( # ` F ) ) )
13 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
14 13 oveq2d 
 |-  ( F ( Walks ` G ) P -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
15 revlen 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` ( reverse ` P ) ) = ( # ` P ) )
16 6 15 syl 
 |-  ( F ( Walks ` G ) P -> ( # ` ( reverse ` P ) ) = ( # ` P ) )
17 16 oveq2d 
 |-  ( F ( Walks ` G ) P -> ( 0 ..^ ( # ` ( reverse ` P ) ) ) = ( 0 ..^ ( # ` P ) ) )
18 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
19 18 nn0zd 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. ZZ )
20 fzval3 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
21 19 20 syl 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
22 14 17 21 3eqtr4rd 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` ( reverse ` P ) ) ) )
23 12 22 eqtrd 
 |-  ( F ( Walks ` G ) P -> ( 0 ... ( # ` ( reverse ` F ) ) ) = ( 0 ..^ ( # ` ( reverse ` P ) ) ) )
24 23 feq2d 
 |-  ( F ( Walks ` G ) P -> ( ( reverse ` P ) : ( 0 ... ( # ` ( reverse ` F ) ) ) --> ( Vtx ` G ) <-> ( reverse ` P ) : ( 0 ..^ ( # ` ( reverse ` P ) ) ) --> ( Vtx ` G ) ) )
25 9 24 mpbird 
 |-  ( F ( Walks ` G ) P -> ( reverse ` P ) : ( 0 ... ( # ` ( reverse ` F ) ) ) --> ( Vtx ` G ) )
26 11 oveq2d 
 |-  ( F ( Walks ` G ) P -> ( 0 ..^ ( # ` ( reverse ` F ) ) ) = ( 0 ..^ ( # ` F ) ) )
27 26 eleq2d 
 |-  ( F ( Walks ` G ) P -> ( k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) <-> k e. ( 0 ..^ ( # ` F ) ) ) )
28 27 biimpa 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) ) -> k e. ( 0 ..^ ( # ` F ) ) )
29 revfv 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` F ) ` k ) = ( F ` ( ( ( # ` F ) - 1 ) - k ) ) )
30 2 29 sylan 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` F ) ` k ) = ( F ` ( ( ( # ` F ) - 1 ) - k ) ) )
31 wlklenvm1 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) = ( ( # ` P ) - 1 ) )
32 31 oveq1d 
 |-  ( F ( Walks ` G ) P -> ( ( # ` F ) - 1 ) = ( ( ( # ` P ) - 1 ) - 1 ) )
33 lencl 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` P ) e. NN0 )
34 33 nn0cnd 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` P ) e. CC )
35 sub1m1 
 |-  ( ( # ` P ) e. CC -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
36 6 34 35 3syl 
 |-  ( F ( Walks ` G ) P -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
37 32 36 eqtrd 
 |-  ( F ( Walks ` G ) P -> ( ( # ` F ) - 1 ) = ( ( # ` P ) - 2 ) )
38 37 fvoveq1d 
 |-  ( F ( Walks ` G ) P -> ( F ` ( ( ( # ` F ) - 1 ) - k ) ) = ( F ` ( ( ( # ` P ) - 2 ) - k ) ) )
39 38 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( ( ( # ` F ) - 1 ) - k ) ) = ( F ` ( ( ( # ` P ) - 2 ) - k ) ) )
40 30 39 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` F ) ` k ) = ( F ` ( ( ( # ` P ) - 2 ) - k ) ) )
41 40 fveq2d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) )
42 41 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) )
43 fzonn0p1p1 
 |-  ( k e. ( 0 ..^ ( # ` F ) ) -> ( k + 1 ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
44 43 adantl 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( k + 1 ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
45 14 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
46 44 45 eleqtrrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( k + 1 ) e. ( 0 ..^ ( # ` P ) ) )
47 revfv 
 |-  ( ( P e. Word ( Vtx ` G ) /\ ( k + 1 ) e. ( 0 ..^ ( # ` P ) ) ) -> ( ( reverse ` P ) ` ( k + 1 ) ) = ( P ` ( ( ( # ` P ) - 1 ) - ( k + 1 ) ) ) )
48 6 46 47 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` P ) ` ( k + 1 ) ) = ( P ` ( ( ( # ` P ) - 1 ) - ( k + 1 ) ) ) )
49 elfzoelz 
 |-  ( k e. ( 0 ..^ ( # ` F ) ) -> k e. ZZ )
50 49 zcnd 
 |-  ( k e. ( 0 ..^ ( # ` F ) ) -> k e. CC )
51 50 adantl 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> k e. CC )
52 1cnd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> 1 e. CC )
53 51 52 addcomd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( k + 1 ) = ( 1 + k ) )
54 53 oveq2d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` P ) - 1 ) - ( k + 1 ) ) = ( ( ( # ` P ) - 1 ) - ( 1 + k ) ) )
55 6 34 syl 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) e. CC )
56 55 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` P ) e. CC )
57 56 52 subcld 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` P ) - 1 ) e. CC )
58 57 52 51 subsub4d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) = ( ( ( # ` P ) - 1 ) - ( 1 + k ) ) )
59 36 oveq1d 
 |-  ( F ( Walks ` G ) P -> ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) = ( ( ( # ` P ) - 2 ) - k ) )
60 59 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) = ( ( ( # ` P ) - 2 ) - k ) )
61 54 58 60 3eqtr2d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` P ) - 1 ) - ( k + 1 ) ) = ( ( ( # ` P ) - 2 ) - k ) )
62 61 fveq2d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` ( ( ( # ` P ) - 1 ) - ( k + 1 ) ) ) = ( P ` ( ( ( # ` P ) - 2 ) - k ) ) )
63 48 62 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` P ) ` ( k + 1 ) ) = ( P ` ( ( ( # ` P ) - 2 ) - k ) ) )
64 63 sneqd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> { ( ( reverse ` P ) ` ( k + 1 ) ) } = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } )
65 64 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> { ( ( reverse ` P ) ` ( k + 1 ) ) } = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } )
66 sneq 
 |-  ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) -> { ( ( reverse ` P ) ` k ) } = { ( ( reverse ` P ) ` ( k + 1 ) ) } )
67 66 adantl 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> { ( ( reverse ` P ) ` k ) } = { ( ( reverse ` P ) ` ( k + 1 ) ) } )
68 eqcom 
 |-  ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) <-> ( ( reverse ` P ) ` ( k + 1 ) ) = ( ( reverse ` P ) ` k ) )
69 fzossfzop1 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( ( # ` F ) + 1 ) ) )
70 18 69 syl 
 |-  ( F ( Walks ` G ) P -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( ( # ` F ) + 1 ) ) )
71 70 14 sseqtrrd 
 |-  ( F ( Walks ` G ) P -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` P ) ) )
72 71 sselda 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> k e. ( 0 ..^ ( # ` P ) ) )
73 revfv 
 |-  ( ( P e. Word ( Vtx ` G ) /\ k e. ( 0 ..^ ( # ` P ) ) ) -> ( ( reverse ` P ) ` k ) = ( P ` ( ( ( # ` P ) - 1 ) - k ) ) )
74 6 72 73 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` P ) ` k ) = ( P ` ( ( ( # ` P ) - 1 ) - k ) ) )
75 57 51 52 sub32d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( # ` P ) - 1 ) - k ) - 1 ) = ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) )
76 75 oveq1d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( ( # ` P ) - 1 ) - k ) - 1 ) + 1 ) = ( ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) + 1 ) )
77 57 51 subcld 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` P ) - 1 ) - k ) e. CC )
78 77 52 npcand 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( ( # ` P ) - 1 ) - k ) - 1 ) + 1 ) = ( ( ( # ` P ) - 1 ) - k ) )
79 59 oveq1d 
 |-  ( F ( Walks ` G ) P -> ( ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) + 1 ) = ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) )
80 79 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( ( # ` P ) - 1 ) - 1 ) - k ) + 1 ) = ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) )
81 76 78 80 3eqtr3d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` P ) - 1 ) - k ) = ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) )
82 81 fveq2d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` ( ( ( # ` P ) - 1 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) )
83 74 82 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( reverse ` P ) ` k ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) )
84 63 83 eqeq12d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( reverse ` P ) ` ( k + 1 ) ) = ( ( reverse ` P ) ` k ) <-> ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) ) )
85 68 84 syl5bb 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) <-> ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) ) )
86 wkslem1 
 |-  ( x = ( ( ( # ` P ) - 2 ) - 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 ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) , ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } , { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) ) )
87 5 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 ) ) ) ) )
88 87 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 ) ) ) )
89 88 adantr 
 |-  ( ( F ( Walks ` G ) P /\ 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 ) ) ) )
90 18 nn0cnd 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. CC )
91 90 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` F ) e. CC )
92 91 51 52 sub32d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` F ) - k ) - 1 ) = ( ( ( # ` F ) - 1 ) - k ) )
93 37 adantr 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` F ) - 1 ) = ( ( # ` P ) - 2 ) )
94 93 oveq1d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` F ) - 1 ) - k ) = ( ( ( # ` P ) - 2 ) - k ) )
95 92 94 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` F ) - k ) - 1 ) = ( ( ( # ` P ) - 2 ) - k ) )
96 ubmelm1fzo 
 |-  ( k e. ( 0 ..^ ( # ` F ) ) -> ( ( ( # ` F ) - k ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
97 96 adantl 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` F ) - k ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
98 95 97 eqeltrrd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` P ) - 2 ) - k ) e. ( 0 ..^ ( # ` F ) ) )
99 86 89 98 rspcdva 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> if- ( ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) , ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } , { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) )
100 dfifp2 
 |-  ( if- ( ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) , ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } , { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) <-> ( ( ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } ) /\ ( -. ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) ) )
101 99 100 sylib 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } ) /\ ( -. ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) ) )
102 101 simpld 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } ) )
103 85 102 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } ) )
104 103 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) } )
105 65 67 104 3eqtr4rd 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) = { ( ( reverse ` P ) ` k ) } )
106 42 105 eqtrd 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } )
107 85 notbid 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) <-> -. ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) ) )
108 101 simprd 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( -. ( P ` ( ( ( # ` P ) - 2 ) - k ) ) = ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) -> { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) )
109 107 108 sylbid 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) -> { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) ) )
110 109 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) )
111 prcom 
 |-  { ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( reverse ` P ) ` k ) } = { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) }
112 63 83 preq12d 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> { ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( reverse ` P ) ` k ) } = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } )
113 111 112 eqtr3id 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } )
114 113 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } = { ( P ` ( ( ( # ` P ) - 2 ) - k ) ) , ( P ` ( ( ( ( # ` P ) - 2 ) - k ) + 1 ) ) } )
115 41 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = ( ( iEdg ` G ) ` ( F ` ( ( ( # ` P ) - 2 ) - k ) ) ) )
116 110 114 115 3sstr4d 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) ) -> { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) )
117 106 116 ifpimpda 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> if- ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } , { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) ) )
118 28 117 syldan 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) ) -> if- ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } , { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) ) )
119 118 ralrimiva 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) if- ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } , { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) ) )
120 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
121 120 simp1d 
 |-  ( F ( Walks ` G ) P -> G e. _V )
122 5 1 iswlkg 
 |-  ( G e. _V -> ( ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) <-> ( ( reverse ` F ) e. Word dom ( iEdg ` G ) /\ ( reverse ` P ) : ( 0 ... ( # ` ( reverse ` F ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) if- ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } , { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) ) ) ) )
123 121 122 syl 
 |-  ( F ( Walks ` G ) P -> ( ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) <-> ( ( reverse ` F ) e. Word dom ( iEdg ` G ) /\ ( reverse ` P ) : ( 0 ... ( # ` ( reverse ` F ) ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` ( reverse ` F ) ) ) if- ( ( ( reverse ` P ) ` k ) = ( ( reverse ` P ) ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) = { ( ( reverse ` P ) ` k ) } , { ( ( reverse ` P ) ` k ) , ( ( reverse ` P ) ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( ( reverse ` F ) ` k ) ) ) ) ) )
124 4 25 119 123 mpbir3and 
 |-  ( F ( Walks ` G ) P -> ( reverse ` F ) ( Walks ` G ) ( reverse ` P ) )