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	$⊢ φ \to W \in Word D$
	swrdf1.m	$⊢ φ \to M \in (0 \dots N)$
	swrdf1.n	$⊢ φ \to N \in (0 \dots \|W\|)$
	swrdf1.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
	swrdrndisj.1	$⊢ φ \to O \in (N \dots P)$
	swrdrndisj.2	$⊢ φ \to P \in (N \dots \|W\|)$
Assertion	swrdrndisj	$⊢ φ \to ran (W substr ⟨M, N⟩) \cap ran (W substr ⟨O, P⟩) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		swrdf1.w	$⊢ φ \to W \in Word D$
2		swrdf1.m	$⊢ φ \to M \in (0 \dots N)$
3		swrdf1.n	$⊢ φ \to N \in (0 \dots \|W\|)$
4		swrdf1.1	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
5		swrdrndisj.1	$⊢ φ \to O \in (N \dots P)$
6		swrdrndisj.2	$⊢ φ \to P \in (N \dots \|W\|)$
7		swrdrn3	$⊢ (W \in Word D \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) = W [(M ..^N)]$
8	1 2 3 7	syl3anc	$⊢ φ \to ran (W substr ⟨M, N⟩) = W [(M ..^N)]$
9		elfzuz	$⊢ N \in (0 \dots \|W\|) \to N \in ℤ_{\geq 0}$
10		fzss1	$⊢ N \in ℤ_{\geq 0} \to (N \dots P) \subseteq (0 \dots P)$
11	3 9 10	3syl	$⊢ φ \to (N \dots P) \subseteq (0 \dots P)$
12	11 5	sseldd	$⊢ φ \to O \in (0 \dots P)$
13		fzss1	$⊢ N \in ℤ_{\geq 0} \to (N \dots \|W\|) \subseteq (0 \dots \|W\|)$
14	3 9 13	3syl	$⊢ φ \to (N \dots \|W\|) \subseteq (0 \dots \|W\|)$
15	14 6	sseldd	$⊢ φ \to P \in (0 \dots \|W\|)$
16		swrdrn3	$⊢ (W \in Word D \land O \in (0 \dots P) \land P \in (0 \dots \|W\|)) \to ran (W substr ⟨O, P⟩) = W [(O ..^P)]$
17	1 12 15 16	syl3anc	$⊢ φ \to ran (W substr ⟨O, P⟩) = W [(O ..^P)]$
18	8 17	ineq12d	$⊢ φ \to ran (W substr ⟨M, N⟩) \cap ran (W substr ⟨O, P⟩) = W [(M ..^N)] \cap W [(O ..^P)]$
19		df-f1	$⊢ W : dom W \underset{1-1}{⟶} D \leftrightarrow (W : dom W ⟶ D \land Fun W^{-1})$
20	19	simprbi	$⊢ W : dom W \underset{1-1}{⟶} D \to Fun W^{-1}$
21		imain	$⊢ Fun W^{-1} \to W [(M ..^N) \cap (O ..^P)] = W [(M ..^N)] \cap W [(O ..^P)]$
22	4 20 21	3syl	$⊢ φ \to W [(M ..^N) \cap (O ..^P)] = W [(M ..^N)] \cap W [(O ..^P)]$
23		elfzuz	$⊢ O \in (N \dots P) \to O \in ℤ_{\geq N}$
24		fzoss1	$⊢ O \in ℤ_{\geq N} \to (O ..^P) \subseteq (N ..^P)$
25	5 23 24	3syl	$⊢ φ \to (O ..^P) \subseteq (N ..^P)$
26		elfzuz3	$⊢ P \in (N \dots \|W\|) \to \|W\| \in ℤ_{\geq P}$
27		fzoss2	$⊢ \|W\| \in ℤ_{\geq P} \to (N ..^P) \subseteq (N ..^\|W\|)$
28	6 26 27	3syl	$⊢ φ \to (N ..^P) \subseteq (N ..^\|W\|)$
29	25 28	sstrd	$⊢ φ \to (O ..^P) \subseteq (N ..^\|W\|)$
30		sslin	$⊢ (O ..^P) \subseteq (N ..^\|W\|) \to (M ..^N) \cap (O ..^P) \subseteq (M ..^N) \cap (N ..^\|W\|)$
31	29 30	syl	$⊢ φ \to (M ..^N) \cap (O ..^P) \subseteq (M ..^N) \cap (N ..^\|W\|)$
32		fzodisj	$⊢ (M ..^N) \cap (N ..^\|W\|) = \emptyset$
33	31 32	sseqtrdi	$⊢ φ \to (M ..^N) \cap (O ..^P) \subseteq \emptyset$
34		ss0	$⊢ (M ..^N) \cap (O ..^P) \subseteq \emptyset \to (M ..^N) \cap (O ..^P) = \emptyset$
35	33 34	syl	$⊢ φ \to (M ..^N) \cap (O ..^P) = \emptyset$
36	35	imaeq2d	$⊢ φ \to W [(M ..^N) \cap (O ..^P)] = W [\emptyset]$
37		ima0	$⊢ W [\emptyset] = \emptyset$
38	36 37	eqtrdi	$⊢ φ \to W [(M ..^N) \cap (O ..^P)] = \emptyset$
39	18 22 38	3eqtr2d	$⊢ φ \to ran (W substr ⟨M, N⟩) \cap ran (W substr ⟨O, P⟩) = \emptyset$

Metamath Proof Explorer

Theorem swrdrndisj

Proof