This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdrndisj

Description: Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-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 )
swrdrndisj.1 
|- ( ph -> O e. ( N ... P ) )
swrdrndisj.2 
|- ( ph -> P e. ( N ... ( # ` W ) ) )
Assertion swrdrndisj 
|- ( ph -> ( ran ( W substr <. M , N >. ) i^i ran ( W substr <. O , P >. ) ) = (/) )

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 swrdrndisj.1 
 |-  ( ph -> O e. ( N ... P ) )
6 swrdrndisj.2 
 |-  ( ph -> P e. ( N ... ( # ` W ) ) )
7 swrdrn3 
 |-  ( ( W e. Word D /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) = ( W " ( M ..^ N ) ) )
8 1 2 3 7 syl3anc 
 |-  ( ph -> ran ( W substr <. M , N >. ) = ( W " ( M ..^ N ) ) )
9 elfzuz 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. ( ZZ>= ` 0 ) )
10 fzss1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( N ... P ) C_ ( 0 ... P ) )
11 3 9 10 3syl 
 |-  ( ph -> ( N ... P ) C_ ( 0 ... P ) )
12 11 5 sseldd 
 |-  ( ph -> O e. ( 0 ... P ) )
13 fzss1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( N ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) ) )
14 3 9 13 3syl 
 |-  ( ph -> ( N ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) ) )
15 14 6 sseldd 
 |-  ( ph -> P e. ( 0 ... ( # ` W ) ) )
16 swrdrn3 
 |-  ( ( W e. Word D /\ O e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. O , P >. ) = ( W " ( O ..^ P ) ) )
17 1 12 15 16 syl3anc 
 |-  ( ph -> ran ( W substr <. O , P >. ) = ( W " ( O ..^ P ) ) )
18 8 17 ineq12d 
 |-  ( ph -> ( ran ( W substr <. M , N >. ) i^i ran ( W substr <. O , P >. ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) )
19 df-f1 
 |-  ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
20 19 simprbi 
 |-  ( W : dom W -1-1-> D -> Fun `' W )
21 imain 
 |-  ( Fun `' W -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) )
22 4 20 21 3syl 
 |-  ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) )
23 elfzuz 
 |-  ( O e. ( N ... P ) -> O e. ( ZZ>= ` N ) )
24 fzoss1 
 |-  ( O e. ( ZZ>= ` N ) -> ( O ..^ P ) C_ ( N ..^ P ) )
25 5 23 24 3syl 
 |-  ( ph -> ( O ..^ P ) C_ ( N ..^ P ) )
26 elfzuz3 
 |-  ( P e. ( N ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` P ) )
27 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` P ) -> ( N ..^ P ) C_ ( N ..^ ( # ` W ) ) )
28 6 26 27 3syl 
 |-  ( ph -> ( N ..^ P ) C_ ( N ..^ ( # ` W ) ) )
29 25 28 sstrd 
 |-  ( ph -> ( O ..^ P ) C_ ( N ..^ ( # ` W ) ) )
30 sslin 
 |-  ( ( O ..^ P ) C_ ( N ..^ ( # ` W ) ) -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) )
31 29 30 syl 
 |-  ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) )
32 fzodisj 
 |-  ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) = (/)
33 31 32 sseqtrdi 
 |-  ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ (/) )
34 ss0 
 |-  ( ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ (/) -> ( ( M ..^ N ) i^i ( O ..^ P ) ) = (/) )
35 33 34 syl 
 |-  ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) = (/) )
36 35 imaeq2d 
 |-  ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( W " (/) ) )
37 ima0 
 |-  ( W " (/) ) = (/)
38 36 37 eqtrdi 
 |-  ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = (/) )
39 18 22 38 3eqtr2d 
 |-  ( ph -> ( ran ( W substr <. M , N >. ) i^i ran ( W substr <. O , P >. ) ) = (/) )