Metamath Proof Explorer

Theorem swrdrevpfx

Description: A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 fznn0sub2 
 |-  ( F e. ( 0 ... L ) -> ( L - F ) e. ( 0 ... L ) )
2 pfxcl 
 |-  ( W e. Word V -> ( W prefix L ) e. Word V )
3 revcl 
 |-  ( ( W prefix L ) e. Word V -> ( reverse ` ( W prefix L ) ) e. Word V )
4 2 3 syl 
 |-  ( W e. Word V -> ( reverse ` ( W prefix L ) ) e. Word V )
5 4 3ad2ant1 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( reverse ` ( W prefix L ) ) e. Word V )
6 simp3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( L - F ) e. ( 0 ... L ) )
7 revlen 
 |-  ( ( W prefix L ) e. Word V -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
8 2 7 syl 
 |-  ( W e. Word V -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
9 8 adantr 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = ( # ` ( W prefix L ) ) )
10 pfxlen 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
11 9 10 eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = L )
12 11 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = L )
13 12 oveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) = ( 0 ... L ) )
14 6 13 eleqtrrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( L - F ) e. ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) )
15 5 14 jca 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - F ) e. ( 0 ... L ) ) -> ( ( reverse ` ( W prefix L ) ) e. Word V /\ ( L - F ) e. ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) ) )
16 1 15 syl3an3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ F e. ( 0 ... L ) ) -> ( ( reverse ` ( W prefix L ) ) e. Word V /\ ( L - F ) e. ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) ) )
17 16 3com23 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( reverse ` ( W prefix L ) ) e. Word V /\ ( L - F ) e. ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) ) )
18 revpfxsfxrev 
 |-  ( ( ( reverse ` ( W prefix L ) ) e. Word V /\ ( L - F ) e. ( 0 ... ( # ` ( reverse ` ( W prefix L ) ) ) ) ) -> ( reverse ` ( ( reverse ` ( W prefix L ) ) prefix ( L - F ) ) ) = ( ( reverse ` ( reverse ` ( W prefix L ) ) ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) )
19 17 18 syl 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( ( reverse ` ( W prefix L ) ) prefix ( L - F ) ) ) = ( ( reverse ` ( reverse ` ( W prefix L ) ) ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) )
20 revrev 
 |-  ( ( W prefix L ) e. Word V -> ( reverse ` ( reverse ` ( W prefix L ) ) ) = ( W prefix L ) )
21 2 20 syl 
 |-  ( W e. Word V -> ( reverse ` ( reverse ` ( W prefix L ) ) ) = ( W prefix L ) )
22 21 oveq1d 
 |-  ( W e. Word V -> ( ( reverse ` ( reverse ` ( W prefix L ) ) ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) = ( ( W prefix L ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) )
23 22 3ad2ant1 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( reverse ` ( reverse ` ( W prefix L ) ) ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) = ( ( W prefix L ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) )
24 11 oveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) = ( L - ( L - F ) ) )
25 24 3adant2 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) = ( L - ( L - F ) ) )
26 elfzel2 
 |-  ( F e. ( 0 ... L ) -> L e. ZZ )
27 26 zcnd 
 |-  ( F e. ( 0 ... L ) -> L e. CC )
28 elfzelz 
 |-  ( F e. ( 0 ... L ) -> F e. ZZ )
29 28 zcnd 
 |-  ( F e. ( 0 ... L ) -> F e. CC )
30 27 29 nncand 
 |-  ( F e. ( 0 ... L ) -> ( L - ( L - F ) ) = F )
31 30 3ad2ant2 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( L - ( L - F ) ) = F )
32 25 31 eqtrd 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) = F )
33 11 3adant2 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( reverse ` ( W prefix L ) ) ) = L )
34 32 33 opeq12d 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. = <. F , L >. )
35 34 oveq2d 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix L ) substr <. ( ( # ` ( reverse ` ( W prefix L ) ) ) - ( L - F ) ) , ( # ` ( reverse ` ( W prefix L ) ) ) >. ) = ( ( W prefix L ) substr <. F , L >. ) )
36 19 23 35 3eqtrd 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( reverse ` ( ( reverse ` ( W prefix L ) ) prefix ( L - F ) ) ) = ( ( W prefix L ) substr <. F , L >. ) )
37 elfzuz3 
 |-  ( F e. ( 0 ... L ) -> L e. ( ZZ>= ` F ) )
38 eluzfz2 
 |-  ( L e. ( ZZ>= ` F ) -> L e. ( F ... L ) )
39 37 38 syl 
 |-  ( F e. ( 0 ... L ) -> L e. ( F ... L ) )
40 39 ancli 
 |-  ( F e. ( 0 ... L ) -> ( F e. ( 0 ... L ) /\ L e. ( F ... L ) ) )
41 40 3ad2ant2 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( F e. ( 0 ... L ) /\ L e. ( F ... L ) ) )
42 swrdpfx 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( F e. ( 0 ... L ) /\ L e. ( F ... L ) ) -> ( ( W prefix L ) substr <. F , L >. ) = ( W substr <. F , L >. ) ) )
43 41 42 syl5 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix L ) substr <. F , L >. ) = ( W substr <. F , L >. ) ) )
44 43 3adant2 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix L ) substr <. F , L >. ) = ( W substr <. F , L >. ) ) )
45 44 pm2.43i 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix L ) substr <. F , L >. ) = ( W substr <. F , L >. ) )
46 36 45 eqtr2d 
 |-  ( ( W e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. F , L >. ) = ( reverse ` ( ( reverse ` ( W prefix L ) ) prefix ( L - F ) ) ) )