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 sseldi 
 |-  ( ( ( ( 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 sseldi 
 |-  ( ( ( ( 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 fzssz 
 |-  ( 0 ... N ) C_ ZZ
20 19 2 sseldi 
 |-  ( ph -> M e. ZZ )
21 20 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 )
22 21 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 )
23 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 )
24 elfzuz 
 |-  ( M e. ( 0 ... N ) -> M e. ( ZZ>= ` 0 ) )
25 fzoss1 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( M ..^ N ) C_ ( 0 ..^ N ) )
26 2 24 25 3syl 
 |-  ( ph -> ( M ..^ N ) C_ ( 0 ..^ N ) )
27 elfzuz3 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
28 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
29 3 27 28 3syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
30 26 29 sstrd 
 |-  ( ph -> ( M ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
31 30 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 ) ) )
32 elfzelz 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. ZZ )
33 3 32 syl 
 |-  ( ph -> N e. ZZ )
34 33 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 )
35 fzoaddel2 
 |-  ( ( i e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( i + M ) e. ( M ..^ N ) )
36 12 34 21 35 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 ) )
37 31 36 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 ) ) )
38 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
39 1 38 syl 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
40 39 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 ) ) )
41 37 40 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 )
42 fzoaddel2 
 |-  ( ( j e. ( 0 ..^ ( N - M ) ) /\ N e. ZZ /\ M e. ZZ ) -> ( j + M ) e. ( M ..^ N ) )
43 16 34 21 42 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 ) )
44 31 43 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 ) ) )
45 44 40 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 )
46 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 ) )
47 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 )
48 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 ) )
49 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 ) ) )
50 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 ) ) )
51 47 48 49 12 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 >. ) ` i ) = ( W ` ( i + M ) ) )
52 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 ) ) )
53 47 48 49 16 52 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 ) ) )
54 46 51 53 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 ) ) )
55 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 ) ) )
56 55 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 ) ) )
57 56 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 ) )
58 23 41 45 54 57 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 ) )
59 14 18 22 58 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 )
60 59 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 ) )
61 60 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 ) )
62 61 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 ) )
63 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 ) ) )
64 7 62 63 sylanbrc 
 |-  ( ph -> ( W substr <. M , N >. ) : dom ( W substr <. M , N >. ) -1-1-> D )