Metamath Proof Explorer

Theorem swrdpfx

Description: A subword of a prefix is a subword. (Contributed by Alexander van der Vekens, 6-Apr-2018) (Revised by AV, 8-May-2020)

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

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. NN0 )
2 1 anim2i 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word V /\ N e. NN0 ) )
3 2 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( W e. Word V /\ N e. NN0 ) )
4 pfxval 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
5 3 4 syl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
6 5 oveq1d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( ( W substr <. 0 , N >. ) substr <. K , L >. ) )
7 simpl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> W e. Word V )
8 simpr 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
9 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
10 1 9 syl 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> 0 e. ( 0 ... N ) )
11 10 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> 0 e. ( 0 ... N ) )
12 7 8 11 3jca 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ... N ) ) )
13 12 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ... N ) ) )
14 elfzelz 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. ZZ )
15 zcn 
 |-  ( N e. ZZ -> N e. CC )
16 15 subid1d 
 |-  ( N e. ZZ -> ( N - 0 ) = N )
17 16 eqcomd 
 |-  ( N e. ZZ -> N = ( N - 0 ) )
18 14 17 syl 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N = ( N - 0 ) )
19 18 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> N = ( N - 0 ) )
20 19 oveq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( 0 ... N ) = ( 0 ... ( N - 0 ) ) )
21 20 eleq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( K e. ( 0 ... N ) <-> K e. ( 0 ... ( N - 0 ) ) ) )
22 19 oveq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( K ... N ) = ( K ... ( N - 0 ) ) )
23 22 eleq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( L e. ( K ... N ) <-> L e. ( K ... ( N - 0 ) ) ) )
24 21 23 anbi12d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) <-> ( K e. ( 0 ... ( N - 0 ) ) /\ L e. ( K ... ( N - 0 ) ) ) ) )
25 24 biimpa 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( K e. ( 0 ... ( N - 0 ) ) /\ L e. ( K ... ( N - 0 ) ) ) )
26 swrdswrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - 0 ) ) /\ L e. ( K ... ( N - 0 ) ) ) -> ( ( W substr <. 0 , N >. ) substr <. K , L >. ) = ( W substr <. ( 0 + K ) , ( 0 + L ) >. ) ) )
27 13 25 26 sylc 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( ( W substr <. 0 , N >. ) substr <. K , L >. ) = ( W substr <. ( 0 + K ) , ( 0 + L ) >. ) )
28 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
29 28 zcnd 
 |-  ( K e. ( 0 ... N ) -> K e. CC )
30 29 adantr 
 |-  ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> K e. CC )
31 30 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> K e. CC )
32 31 addid2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( 0 + K ) = K )
33 elfzelz 
 |-  ( L e. ( K ... N ) -> L e. ZZ )
34 33 zcnd 
 |-  ( L e. ( K ... N ) -> L e. CC )
35 34 adantl 
 |-  ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> L e. CC )
36 35 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> L e. CC )
37 36 addid2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( 0 + L ) = L )
38 32 37 opeq12d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> <. ( 0 + K ) , ( 0 + L ) >. = <. K , L >. )
39 38 oveq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( W substr <. ( 0 + K ) , ( 0 + L ) >. ) = ( W substr <. K , L >. ) )
40 6 27 39 3eqtrd 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( W substr <. K , L >. ) )
41 40 ex 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( W substr <. K , L >. ) ) )