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 ( 𝜑𝑊 ∈ Word 𝐷 )
swrdf1.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
swrdf1.n ( 𝜑𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
swrdf1.1 ( 𝜑𝑊 : dom 𝑊1-1𝐷 )
swrdrndisj.1 ( 𝜑𝑂 ∈ ( 𝑁 ... 𝑃 ) )
swrdrndisj.2 ( 𝜑𝑃 ∈ ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) )
Assertion swrdrndisj ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝑂 , 𝑃 ⟩ ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 swrdf1.w ( 𝜑𝑊 ∈ Word 𝐷 )
2 swrdf1.m ( 𝜑𝑀 ∈ ( 0 ... 𝑁 ) )
3 swrdf1.n ( 𝜑𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 swrdf1.1 ( 𝜑𝑊 : dom 𝑊1-1𝐷 )
5 swrdrndisj.1 ( 𝜑𝑂 ∈ ( 𝑁 ... 𝑃 ) )
6 swrdrndisj.2 ( 𝜑𝑃 ∈ ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) )
7 swrdrn3 ( ( 𝑊 ∈ Word 𝐷𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) )
8 1 2 3 7 syl3anc ( 𝜑 → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) )
9 elfzuz ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
10 fzss1 ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 𝑁 ... 𝑃 ) ⊆ ( 0 ... 𝑃 ) )
11 3 9 10 3syl ( 𝜑 → ( 𝑁 ... 𝑃 ) ⊆ ( 0 ... 𝑃 ) )
12 11 5 sseldd ( 𝜑𝑂 ∈ ( 0 ... 𝑃 ) )
13 fzss1 ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
14 3 9 13 3syl ( 𝜑 → ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
15 14 6 sseldd ( 𝜑𝑃 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
16 swrdrn3 ( ( 𝑊 ∈ Word 𝐷𝑂 ∈ ( 0 ... 𝑃 ) ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑂 , 𝑃 ⟩ ) = ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) )
17 1 12 15 16 syl3anc ( 𝜑 → ran ( 𝑊 substr ⟨ 𝑂 , 𝑃 ⟩ ) = ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) )
18 8 17 ineq12d ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝑂 , 𝑃 ⟩ ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) )
19 df-f1 ( 𝑊 : dom 𝑊1-1𝐷 ↔ ( 𝑊 : dom 𝑊𝐷 ∧ Fun 𝑊 ) )
20 19 simprbi ( 𝑊 : dom 𝑊1-1𝐷 → Fun 𝑊 )
21 imain ( Fun 𝑊 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) )
22 4 20 21 3syl ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( ( 𝑊 “ ( 𝑀 ..^ 𝑁 ) ) ∩ ( 𝑊 “ ( 𝑂 ..^ 𝑃 ) ) ) )
23 elfzuz ( 𝑂 ∈ ( 𝑁 ... 𝑃 ) → 𝑂 ∈ ( ℤ𝑁 ) )
24 fzoss1 ( 𝑂 ∈ ( ℤ𝑁 ) → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ 𝑃 ) )
25 5 23 24 3syl ( 𝜑 → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ 𝑃 ) )
26 elfzuz3 ( 𝑃 ∈ ( 𝑁 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝑃 ) )
27 fzoss2 ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝑃 ) → ( 𝑁 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) )
28 6 26 27 3syl ( 𝜑 → ( 𝑁 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) )
29 25 28 sstrd ( 𝜑 → ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) )
30 sslin ( ( 𝑂 ..^ 𝑃 ) ⊆ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) )
31 29 30 syl ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) )
32 fzodisj ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑁 ..^ ( ♯ ‘ 𝑊 ) ) ) = ∅
33 31 32 sseqtrdi ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ∅ )
34 ss0 ( ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ⊆ ∅ → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) = ∅ )
35 33 34 syl ( 𝜑 → ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) = ∅ )
36 35 imaeq2d ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ( 𝑊 “ ∅ ) )
37 ima0 ( 𝑊 “ ∅ ) = ∅
38 36 37 eqtrdi ( 𝜑 → ( 𝑊 “ ( ( 𝑀 ..^ 𝑁 ) ∩ ( 𝑂 ..^ 𝑃 ) ) ) = ∅ )
39 18 22 38 3eqtr2d ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝑂 , 𝑃 ⟩ ) ) = ∅ )