swrdf1

Description: Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-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$
Assertion	swrdf1	$⊢ φ \to (W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) \underset{1-1}{⟶} D$

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		swrdf	$⊢ (W \in Word D \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ D$
6	1 2 3 5	syl3anc	$⊢ φ \to (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ D$
7	6	ffdmd	$⊢ φ \to (W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) ⟶ D$
8		fzossz	$⊢ (0 ..^N - M) \subseteq ℤ$
9		simpllr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i \in dom (W substr ⟨M, N⟩)$
10	6	fdmd	$⊢ φ \to dom (W substr ⟨M, N⟩) = (0 ..^N - M)$
11	10	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to dom (W substr ⟨M, N⟩) = (0 ..^N - M)$
12	9 11	eleqtrd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i \in (0 ..^N - M)$
13	8 12	sselid	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i \in ℤ$
14	13	zcnd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i \in ℂ$
15		simplr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j \in dom (W substr ⟨M, N⟩)$
16	15 11	eleqtrd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j \in (0 ..^N - M)$
17	8 16	sselid	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j \in ℤ$
18	17	zcnd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j \in ℂ$
19	2	elfzelzd	$⊢ φ \to M \in ℤ$
20	19	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to M \in ℤ$
21	20	zcnd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to M \in ℂ$
22	4	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to W : dom W \underset{1-1}{⟶} D$
23		elfzuz	$⊢ M \in (0 \dots N) \to M \in ℤ_{\geq 0}$
24		fzoss1	$⊢ M \in ℤ_{\geq 0} \to (M ..^N) \subseteq (0 ..^N)$
25	2 23 24	3syl	$⊢ φ \to (M ..^N) \subseteq (0 ..^N)$
26		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
27		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
28	3 26 27	3syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^\|W\|)$
29	25 28	sstrd	$⊢ φ \to (M ..^N) \subseteq (0 ..^\|W\|)$
30	29	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to (M ..^N) \subseteq (0 ..^\|W\|)$
31	3	elfzelzd	$⊢ φ \to N \in ℤ$
32	31	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to N \in ℤ$
33		fzoaddel2	$⊢ (i \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to i + M \in (M ..^N)$
34	12 32 20 33	syl3anc	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i + M \in (M ..^N)$
35	30 34	sseldd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i + M \in (0 ..^\|W\|)$
36		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
37	1 36	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
38	37	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to dom W = (0 ..^\|W\|)$
39	35 38	eleqtrrd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i + M \in dom W$
40		fzoaddel2	$⊢ (j \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to j + M \in (M ..^N)$
41	16 32 20 40	syl3anc	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j + M \in (M ..^N)$
42	30 41	sseldd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j + M \in (0 ..^\|W\|)$
43	42 38	eleqtrrd	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to j + M \in dom W$
44		simpr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)$
45	1	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to W \in Word D$
46	2	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to M \in (0 \dots N)$
47	3	ad3antrrr	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to N \in (0 \dots \|W\|)$
48		swrdfv	$⊢ ((W \in Word D \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to (W substr ⟨M, N⟩) (i) = W (i + M)$
49	45 46 47 12 48	syl31anc	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to (W substr ⟨M, N⟩) (i) = W (i + M)$
50		swrdfv	$⊢ ((W \in Word D \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (0 ..^N - M)) \to (W substr ⟨M, N⟩) (j) = W (j + M)$
51	45 46 47 16 50	syl31anc	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to (W substr ⟨M, N⟩) (j) = W (j + M)$
52	44 49 51	3eqtr3d	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to W (i + M) = W (j + M)$
53		f1veqaeq	$⊢ (W : dom W \underset{1-1}{⟶} D \land (i + M \in dom W \land j + M \in dom W)) \to (W (i + M) = W (j + M) \to i + M = j + M)$
54	53	anassrs	$⊢ ((W : dom W \underset{1-1}{⟶} D \land i + M \in dom W) \land j + M \in dom W) \to (W (i + M) = W (j + M) \to i + M = j + M)$
55	54	imp	$⊢ (((W : dom W \underset{1-1}{⟶} D \land i + M \in dom W) \land j + M \in dom W) \land W (i + M) = W (j + M)) \to i + M = j + M$
56	22 39 43 52 55	syl1111anc	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i + M = j + M$
57	14 18 21 56	addcan2ad	$⊢ (((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \land (W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j)) \to i = j$
58	57	ex	$⊢ ((φ \land i \in dom (W substr ⟨M, N⟩)) \land j \in dom (W substr ⟨M, N⟩)) \to ((W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j) \to i = j)$
59	58	anasss	$⊢ (φ \land (i \in dom (W substr ⟨M, N⟩) \land j \in dom (W substr ⟨M, N⟩))) \to ((W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j) \to i = j)$
60	59	ralrimivva	$⊢ φ \to \forall i \in dom (W substr ⟨M, N⟩) \forall j \in dom (W substr ⟨M, N⟩) ((W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j) \to i = j)$
61		dff13	$⊢ (W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) \underset{1-1}{⟶} D \leftrightarrow ((W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) ⟶ D \land \forall i \in dom (W substr ⟨M, N⟩) \forall j \in dom (W substr ⟨M, N⟩) ((W substr ⟨M, N⟩) (i) = (W substr ⟨M, N⟩) (j) \to i = j))$
62	7 60 61	sylanbrc	$⊢ φ \to (W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) \underset{1-1}{⟶} D$

Metamath Proof Explorer

Theorem swrdf1

Proof