Metamath Proof Explorer

Theorem revpfxsfxrev

Description: The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023)

Ref Expression
Assertion revpfxsfxrev 
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( W prefix L ) ) = ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) )

Proof

Step Hyp Ref Expression
1 pfxcl 
 |-  ( W e. Word V -> ( W prefix L ) e. Word V )
2 revcl 
 |-  ( ( W prefix L ) e. Word V -> ( reverse ` ( W prefix L ) ) e. Word V )
3 wrdfn 
 |-  ( ( reverse ` ( W prefix L ) ) e. Word V -> ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( W prefix L ) ) ) ) )
4 1 2 3 3syl 
 |-  ( W e. Word V -> ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( W prefix L ) ) ) ) )
5 4 adantr 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( W prefix L ) ) ) ) )
6 revlen 
 |-  ( ( W prefix L ) e. Word V -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
7 1 6 syl 
 |-  ( W e. Word V -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
8 7 adantr 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
9 pfxlen 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
10 8 9 eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = L )
11 10 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( reverse ` ( W prefix L ) ) ) ) = ( 0 ..^ L ) )
12 11 fneq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ ( # ` ( reverse ` ( W prefix L ) ) ) ) <-> ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ L ) ) )
13 5 12 mpbid 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( W prefix L ) ) Fn ( 0 ..^ L ) )
14 revcl 
 |-  ( W e. Word V -> ( reverse ` W ) e. Word V )
15 swrdcl 
 |-  ( ( reverse ` W ) e. Word V -> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) e. Word V )
16 wrdfn 
 |-  ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) e. Word V -> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) ) )
17 14 15 16 3syl 
 |-  ( W e. Word V -> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) ) )
18 17 adantr 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) ) )
19 fznn0sub2 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) )
20 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
21 nn0fz0 
 |-  ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
22 20 21 sylib 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
23 revlen 
 |-  ( W e. Word V -> ( # ` ( reverse ` W ) ) = ( # ` W ) )
24 23 oveq2d 
 |-  ( W e. Word V -> ( 0 ... ( # ` ( reverse ` W ) ) ) = ( 0 ... ( # ` W ) ) )
25 22 24 eleqtrrd 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` ( reverse ` W ) ) ) )
26 swrdlen 
 |-  ( ( ( reverse ` W ) e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` ( reverse ` W ) ) ) ) -> ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( ( # ` W ) - L ) ) )
27 14 19 25 26 syl3an 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ W e. Word V ) -> ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( ( # ` W ) - L ) ) )
28 27 3anidm13 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) = ( ( # ` W ) - ( ( # ` W ) - L ) ) )
29 20 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
30 29 adantr 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. CC )
31 elfzelz 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. ZZ )
32 31 zcnd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. CC )
33 32 adantl 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> L e. CC )
34 30 33 nncand 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` W ) - ( ( # ` W ) - L ) ) = L )
35 28 34 eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) = L )
36 35 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) ) = ( 0 ..^ L ) )
37 36 fneq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ ( # ` ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ) ) <-> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ L ) ) )
38 18 37 mpbid 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) Fn ( 0 ..^ L ) )
39 simp1 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> W e. Word V )
40 simp3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> x e. ( 0 ..^ L ) )
41 9 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( 0 ..^ ( # ` ( W prefix L ) ) ) = ( 0 ..^ L ) )
42 41 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( 0 ..^ ( # ` ( W prefix L ) ) ) = ( 0 ..^ L ) )
43 40 42 eleqtrrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> x e. ( 0 ..^ ( # ` ( W prefix L ) ) ) )
44 revfv 
 |-  ( ( ( W prefix L ) e. Word V /\ x e. ( 0 ..^ ( # ` ( W prefix L ) ) ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( ( W prefix L ) ` ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) ) )
45 1 44 sylan 
 |-  ( ( W e. Word V /\ x e. ( 0 ..^ ( # ` ( W prefix L ) ) ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( ( W prefix L ) ` ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) ) )
46 39 43 45 syl2anc 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( ( W prefix L ) ` ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) ) )
47 9 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix L ) ) - 1 ) = ( L - 1 ) )
48 47 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) = ( ( L - 1 ) - x ) )
49 48 fveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) ) = ( ( W prefix L ) ` ( ( L - 1 ) - x ) ) )
50 49 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` ( ( ( # ` ( W prefix L ) ) - 1 ) - x ) ) = ( ( W prefix L ) ` ( ( L - 1 ) - x ) ) )
51 32 3ad2ant2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> L e. CC )
52 elfzoelz 
 |-  ( x e. ( 0 ..^ L ) -> x e. ZZ )
53 52 zcnd 
 |-  ( x e. ( 0 ..^ L ) -> x e. CC )
54 53 3ad2ant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> x e. CC )
55 1cnd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> 1 e. CC )
56 51 54 55 sub32d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( L - x ) - 1 ) = ( ( L - 1 ) - x ) )
57 ubmelm1fzo 
 |-  ( x e. ( 0 ..^ L ) -> ( ( L - x ) - 1 ) e. ( 0 ..^ L ) )
58 57 3ad2ant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( L - x ) - 1 ) e. ( 0 ..^ L ) )
59 56 58 eqeltrrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( L - 1 ) - x ) e. ( 0 ..^ L ) )
60 pfxfv 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( ( L - 1 ) - x ) e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` ( ( L - 1 ) - x ) ) = ( W ` ( ( L - 1 ) - x ) ) )
61 59 60 syld3an3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` ( ( L - 1 ) - x ) ) = ( W ` ( ( L - 1 ) - x ) ) )
62 46 50 61 3eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( W ` ( ( L - 1 ) - x ) ) )
63 34 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) = ( 0 ..^ L ) )
64 63 eleq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) <-> x e. ( 0 ..^ L ) ) )
65 64 biimp3ar 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) )
66 id 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ W e. Word V ) -> ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ W e. Word V ) )
67 66 3anidm13 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ W e. Word V ) )
68 swrdfv 
 |-  ( ( ( ( reverse ` W ) e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` ( reverse ` W ) ) ) ) /\ x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
69 14 68 syl3anl1 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` ( reverse ` W ) ) ) ) /\ x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
70 25 69 syl3anl3 
 |-  ( ( ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ W e. Word V ) /\ x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
71 67 70 stoic3 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - L ) e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
72 19 71 syl3an2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ ( ( # ` W ) - ( ( # ` W ) - L ) ) ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
73 65 72 syld3an3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) )
74 0z 
 |-  0 e. ZZ
75 elfzuz3 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` L ) )
76 32 addlidd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( 0 + L ) = L )
77 76 fveq2d 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ZZ>= ` ( 0 + L ) ) = ( ZZ>= ` L ) )
78 75 77 eleqtrrd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` ( 0 + L ) ) )
79 eluzsub 
 |-  ( ( 0 e. ZZ /\ L e. ZZ /\ ( # ` W ) e. ( ZZ>= ` ( 0 + L ) ) ) -> ( ( # ` W ) - L ) e. ( ZZ>= ` 0 ) )
80 74 31 78 79 mp3an2i 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - L ) e. ( ZZ>= ` 0 ) )
81 fzoss1 
 |-  ( ( ( # ` W ) - L ) e. ( ZZ>= ` 0 ) -> ( ( ( # ` W ) - L ) ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
82 80 81 syl 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( ( ( # ` W ) - L ) ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
83 82 3ad2ant2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - L ) ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
84 20 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
85 84 3ad2ant1 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( # ` W ) e. ZZ )
86 31 3ad2ant2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> L e. ZZ )
87 85 86 zsubcld 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( # ` W ) - L ) e. ZZ )
88 fzo0addel 
 |-  ( ( x e. ( 0 ..^ L ) /\ ( ( # ` W ) - L ) e. ZZ ) -> ( x + ( ( # ` W ) - L ) ) e. ( ( ( # ` W ) - L ) ..^ ( L + ( ( # ` W ) - L ) ) ) )
89 40 87 88 syl2anc 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( x + ( ( # ` W ) - L ) ) e. ( ( ( # ` W ) - L ) ..^ ( L + ( ( # ` W ) - L ) ) ) )
90 30 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( # ` W ) e. CC )
91 51 90 pncan3d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( L + ( ( # ` W ) - L ) ) = ( # ` W ) )
92 91 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - L ) ..^ ( L + ( ( # ` W ) - L ) ) ) = ( ( ( # ` W ) - L ) ..^ ( # ` W ) ) )
93 89 92 eleqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( x + ( ( # ` W ) - L ) ) e. ( ( ( # ` W ) - L ) ..^ ( # ` W ) ) )
94 83 93 sseldd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( x + ( ( # ` W ) - L ) ) e. ( 0 ..^ ( # ` W ) ) )
95 revfv 
 |-  ( ( W e. Word V /\ ( x + ( ( # ` W ) - L ) ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) ) )
96 39 94 95 syl2anc 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( reverse ` W ) ` ( x + ( ( # ` W ) - L ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) ) )
97 90 55 subcld 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( # ` W ) - 1 ) e. CC )
98 87 zcnd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( # ` W ) - L ) e. CC )
99 97 54 98 sub32d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( ( # ` W ) - 1 ) - x ) - ( ( # ` W ) - L ) ) = ( ( ( ( # ` W ) - 1 ) - ( ( # ` W ) - L ) ) - x ) )
100 97 54 98 subsub4d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( ( # ` W ) - 1 ) - x ) - ( ( # ` W ) - L ) ) = ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) )
101 90 55 98 sub32d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - 1 ) - ( ( # ` W ) - L ) ) = ( ( ( # ` W ) - ( ( # ` W ) - L ) ) - 1 ) )
102 101 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( ( # ` W ) - 1 ) - ( ( # ` W ) - L ) ) - x ) = ( ( ( ( # ` W ) - ( ( # ` W ) - L ) ) - 1 ) - x ) )
103 99 100 102 3eqtr3d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) = ( ( ( ( # ` W ) - ( ( # ` W ) - L ) ) - 1 ) - x ) )
104 34 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( # ` W ) - ( ( # ` W ) - L ) ) = L )
105 104 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - ( ( # ` W ) - L ) ) - 1 ) = ( L - 1 ) )
106 105 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( ( # ` W ) - ( ( # ` W ) - L ) ) - 1 ) - x ) = ( ( L - 1 ) - x ) )
107 103 106 eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) = ( ( L - 1 ) - x ) )
108 107 fveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - ( x + ( ( # ` W ) - L ) ) ) ) = ( W ` ( ( L - 1 ) - x ) ) )
109 73 96 108 3eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) = ( W ` ( ( L - 1 ) - x ) ) )
110 62 109 eqtr4d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) )
111 110 3expa 
 |-  ( ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) /\ x e. ( 0 ..^ L ) ) -> ( ( reverse ` ( W prefix L ) ) ` x ) = ( ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) ` x ) )
112 13 38 111 eqfnfvd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( W prefix L ) ) = ( ( reverse ` W ) substr <. ( ( # ` W ) - L ) , ( # ` W ) >. ) )