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 ⊢ ( 𝜑 → 𝑊 ∈ 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 ⟨ 𝑂 , 𝑃 ⟩ ) ) = ∅ )