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 φ W Word D
swrdf1.m φ M 0 N
swrdf1.n φ N 0 W
swrdf1.1 φ W : dom W 1-1 D
swrdrndisj.1 φ O N P
swrdrndisj.2 φ P N W
Assertion swrdrndisj φ ran W substr M N ran W substr O P =

Proof

Step Hyp Ref Expression
1 swrdf1.w φ W Word D
2 swrdf1.m φ M 0 N
3 swrdf1.n φ N 0 W
4 swrdf1.1 φ W : dom W 1-1 D
5 swrdrndisj.1 φ O N P
6 swrdrndisj.2 φ P N W
7 swrdrn3 W Word D M 0 N N 0 W ran W substr M N = W M ..^ N
8 1 2 3 7 syl3anc φ ran W substr M N = W M ..^ N
9 elfzuz N 0 W N 0
10 fzss1 N 0 N P 0 P
11 3 9 10 3syl φ N P 0 P
12 11 5 sseldd φ O 0 P
13 fzss1 N 0 N W 0 W
14 3 9 13 3syl φ N W 0 W
15 14 6 sseldd φ P 0 W
16 swrdrn3 W Word D O 0 P P 0 W ran W substr O P = W O ..^ P
17 1 12 15 16 syl3anc φ ran W substr O P = W O ..^ P
18 8 17 ineq12d φ ran W substr M N ran W substr O P = W M ..^ N W O ..^ P
19 df-f1 W : dom W 1-1 D W : dom W D Fun W -1
20 19 simprbi W : dom W 1-1 D Fun W -1
21 imain Fun W -1 W M ..^ N O ..^ P = W M ..^ N W O ..^ P
22 4 20 21 3syl φ W M ..^ N O ..^ P = W M ..^ N W O ..^ P
23 elfzuz O N P O N
24 fzoss1 O N O ..^ P N ..^ P
25 5 23 24 3syl φ O ..^ P N ..^ P
26 elfzuz3 P N W W P
27 fzoss2 W P N ..^ P N ..^ W
28 6 26 27 3syl φ N ..^ P N ..^ W
29 25 28 sstrd φ O ..^ P N ..^ W
30 sslin O ..^ P N ..^ W M ..^ N O ..^ P M ..^ N N ..^ W
31 29 30 syl φ M ..^ N O ..^ P M ..^ N N ..^ W
32 fzodisj M ..^ N N ..^ W =
33 31 32 sseqtrdi φ M ..^ N O ..^ P
34 ss0 M ..^ N O ..^ P M ..^ N O ..^ P =
35 33 34 syl φ M ..^ N O ..^ P =
36 35 imaeq2d φ W M ..^ N O ..^ P = W
37 ima0 W =
38 36 37 eqtrdi φ W M ..^ N O ..^ P =
39 18 22 38 3eqtr2d φ ran W substr M N ran W substr O P =