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	sseldi	$⊢ (((φ \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	sseldi	$⊢ (((φ \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		fzssz	$⊢ (0 \dots N) \subseteq ℤ$
20	19 2	sseldi	$⊢ φ \to M \in ℤ$
21	20	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 ℤ$
22	21	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 ℂ$
23	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$
24		elfzuz	$⊢ M \in (0 \dots N) \to M \in ℤ_{\geq 0}$
25		fzoss1	$⊢ M \in ℤ_{\geq 0} \to (M ..^N) \subseteq (0 ..^N)$
26	2 24 25	3syl	$⊢ φ \to (M ..^N) \subseteq (0 ..^N)$
27		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
28		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
29	3 27 28	3syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^\|W\|)$
30	26 29	sstrd	$⊢ φ \to (M ..^N) \subseteq (0 ..^\|W\|)$
31	30	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\|)$
32		elfzelz	$⊢ N \in (0 \dots \|W\|) \to N \in ℤ$
33	3 32	syl	$⊢ φ \to N \in ℤ$
34	33	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 ℤ$
35		fzoaddel2	$⊢ (i \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to i + M \in (M ..^N)$
36	12 34 21 35	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)$
37	31 36	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\|)$
38		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
39	1 38	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
40	39	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\|)$
41	37 40	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$
42		fzoaddel2	$⊢ (j \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to j + M \in (M ..^N)$
43	16 34 21 42	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)$
44	31 43	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\|)$
45	44 40	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$
46		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)$
47	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$
48	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)$
49	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\|)$
50		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)$
51	47 48 49 12 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⟩) (i) = W (i + M)$
52		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)$
53	47 48 49 16 52	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)$
54	46 51 53	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)$
55		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)$
56	55	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)$
57	56	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$
58	23 41 45 54 57	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$
59	14 18 22 58	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$
60	59	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)$
61	60	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)$
62	61	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)$
63		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))$
64	7 62 63	sylanbrc	$⊢ φ \to (W substr ⟨M, N⟩) : dom (W substr ⟨M, N⟩) \underset{1-1}{⟶} D$

Metamath Proof Explorer

Theorem swrdf1

Proof