# 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 = ∅$