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 ⟨ 𝑂 , 𝑃 ⟩ ) ) = ∅ )