Metamath Proof Explorer

Theorem swrdf1

Description: Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023)

Ref Expression
Hypotheses swrdf1.w 
|- ( ph -> W e. Word D )
swrdf1.m 
|- ( ph -> M e. ( 0 ... N ) )
swrdf1.n 
|- ( ph -> N e. ( 0 ... ( # ` W ) ) )
swrdf1.1 
|- ( ph -> W : dom W -1-1-> D )
Assertion swrdf1 
|- ( ph -> ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) -1-1-> D )

Proof

Step Hyp Ref Expression
1 swrdf1.w 
 |-  ( ph -> W e. Word D )
2 swrdf1.m 
 |-  ( ph -> M e. ( 0 ... N ) )
3 swrdf1.n 
 |-  ( ph -> N e. ( 0 ... ( # ` W ) ) )
4 swrdf1.1 
 |-  ( ph -> W : dom W -1-1-> D )
5 swrdf 
 |-  ( ( W e. Word D /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> D )
6 1 2 3 5 syl3anc 
 |-  ( ph -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> D )
7 6 ffdmd 
 |-  ( ph -> ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) --> D )
8 fzossz 
 |-  ( 0 ..^ ( N - M ) ) C_ ZZ
9 simpllr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> i e. dom ( W substr <. M , N >. ) )
10 6 fdmd 
 |-  ( ph -> dom ( W substr <. M , N >. ) = ( 0 ..^ ( N - M ) ) )
11 10 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> dom ( W substr <. M , N >. ) = ( 0 ..^ ( N - M ) ) )
12 9 11 eleqtrd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> i e. ( 0 ..^ ( N - M ) ) )
13 8 12 sselid 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> i e. ZZ )
14 13 zcnd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> i e. CC )
15 simplr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> j e. dom ( W substr <. M , N >. ) )
16 15 11 eleqtrd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> j e. ( 0 ..^ ( N - M ) ) )
17 8 16 sselid 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> j e. ZZ )
18 17 zcnd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> j e. CC )
19 2 elfzelzd 
 |-  ( ph -> M e. ZZ )
20 19 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> M e. ZZ )
21 20 zcnd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> M e. CC )
22 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> W : dom W -1-1-> D )
23 elfzuz 
 |-  ( M e. ( 0 ... N ) -> M e. ( ZZ>= ` 0 ) )
24 fzoss1 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( M ..^ N ) C_ ( 0 ..^ N ) )
25 2 23 24 3syl 
 |-  ( ph -> ( M ..^ N ) C_ ( 0 ..^ N ) )
26 elfzuz3 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
27 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
28 3 26 27 3syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
29 25 28 sstrd 
 |-  ( ph -> ( M ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( M ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
31 3 elfzelzd 
 |-  ( ph -> N e. ZZ )
32 31 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> N e. ZZ )
33 fzoaddel2 
 |-  ( ( i e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( i + M ) e. ( M ..^ N ) )
34 12 32 20 33 syl3anc 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( i + M ) e. ( M ..^ N ) )
35 30 34 sseldd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( i + M ) e. ( 0 ..^ ( # ` W ) ) )
36 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
37 1 36 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
38 37 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> dom W = ( 0 ..^ ( # ` W ) ) )
39 35 38 eleqtrrd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( i + M ) e. dom W )
40 fzoaddel2 
 |-  ( ( j e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( j + M ) e. ( M ..^ N ) )
41 16 32 20 40 syl3anc 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( j + M ) e. ( M ..^ N ) )
42 30 41 sseldd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( j + M ) e. ( 0 ..^ ( # ` W ) ) )
43 42 38 eleqtrrd 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( j + M ) e. dom W )
44 simpr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) )
45 1 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> W e. Word D )
46 2 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> M e. ( 0 ... N ) )
47 3 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> N e. ( 0 ... ( # ` W ) ) )
48 swrdfv 
 |-  ( ( ( W e. Word D /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( W substr <. M , N >. ) ` i ) = ( W ` ( i + M ) ) )
49 45 46 47 12 48 syl31anc 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( ( W substr <. M , N >. ) ` i ) = ( W ` ( i + M ) ) )
50 swrdfv 
 |-  ( ( ( W e. Word D /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ j e. ( 0 ..^ ( N - M ) ) ) -> ( ( W substr <. M , N >. ) ` j ) = ( W ` ( j + M ) ) )
51 45 46 47 16 50 syl31anc 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( ( W substr <. M , N >. ) ` j ) = ( W ` ( j + M ) ) )
52 44 49 51 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( W ` ( i + M ) ) = ( W ` ( j + M ) ) )
53 f1veqaeq 
 |-  ( ( W : dom W -1-1-> D /\ ( ( i + M ) e. dom W /\ ( j + M ) e. dom W ) ) -> ( ( W ` ( i + M ) ) = ( W ` ( j + M ) ) -> ( i + M ) = ( j + M ) ) )
54 53 anassrs 
 |-  ( ( ( W : dom W -1-1-> D /\ ( i + M ) e. dom W ) /\ ( j + M ) e. dom W ) -> ( ( W ` ( i + M ) ) = ( W ` ( j + M ) ) -> ( i + M ) = ( j + M ) ) )
55 54 imp 
 |-  ( ( ( ( W : dom W -1-1-> D /\ ( i + M ) e. dom W ) /\ ( j + M ) e. dom W ) /\ ( W ` ( i + M ) ) = ( W ` ( j + M ) ) ) -> ( i + M ) = ( j + M ) )
56 22 39 43 52 55 syl1111anc 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> ( i + M ) = ( j + M ) )
57 14 18 21 56 addcan2ad 
 |-  ( ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) /\ ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) ) -> i = j )
58 57 ex 
 |-  ( ( ( ph /\ i e. dom ( W substr <. M , N >. ) ) /\ j e. dom ( W substr <. M , N >. ) ) -> ( ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) -> i = j ) )
59 58 anasss 
 |-  ( ( ph /\ ( i e. dom ( W substr <. M , N >. ) /\ j e. dom ( W substr <. M , N >. ) ) ) -> ( ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) -> i = j ) )
60 59 ralrimivva 
 |-  ( ph -> A. i e. dom ( W substr <. M , N >. ) A. j e. dom ( W substr <. M , N >. ) ( ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) -> i = j ) )
61 dff13 
 |-  ( ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) -1-1-> D <-> ( ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) --> D /\ A. i e. dom ( W substr <. M , N >. ) A. j e. dom ( W substr <. M , N >. ) ( ( ( W substr <. M , N >. ) ` i ) = ( ( W substr <. M , N >. ) ` j ) -> i = j ) ) )
62 7 60 61 sylanbrc 
 |-  ( ph -> ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) -1-1-> D )