swrdrn3

Description: Express the range of a subword. Stronger version of swrdrn2 . (Contributed by Thierry Arnoux, 13-Dec-2023)

		Ref	Expression
	Assertion	swrdrn3	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) = W [(M ..^N)]$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to i \in (0 ..^N - M)$
2		simpl3	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to N \in (0 \dots \|W\|)$
3	2	elfzelzd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to N \in ℤ$
4		simpl2	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to M \in (0 \dots N)$
5	4	elfzelzd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to M \in ℤ$
6		fzoaddel2	$⊢ (i \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to i + M \in (M ..^N)$
7	1 3 5 6	syl3anc	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land i \in (0 ..^N - M)) \to i + M \in (M ..^N)$
8		simpr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j \in (M ..^N)$
9		simpl2	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to M \in (0 \dots N)$
10	9	elfzelzd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to M \in ℤ$
11	10	zcnd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to M \in ℂ$
12		simpl3	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to N \in (0 \dots \|W\|)$
13	12	elfzelzd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to N \in ℤ$
14	13	zcnd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to N \in ℂ$
15	11 14	pncan3d	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to M + N - M = N$
16	15	oveq2d	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to (M ..^M + N - M) = (M ..^N)$
17	8 16	eleqtrrd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j \in (M ..^M + N - M)$
18	13 10	zsubcld	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to N - M \in ℤ$
19		fzosubel3	$⊢ (j \in (M ..^M + N - M) \land N - M \in ℤ) \to j - M \in (0 ..^N - M)$
20	17 18 19	syl2anc	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j - M \in (0 ..^N - M)$
21		simpr	$⊢ (((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \land i = j - M) \to i = j - M$
22	21	oveq1d	$⊢ (((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \land i = j - M) \to i + M = j - M + M$
23	22	eqeq2d	$⊢ (((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \land i = j - M) \to (j = i + M \leftrightarrow j = j - M + M)$
24		fzossz	$⊢ (M ..^N) \subseteq ℤ$
25	24 8	sseldi	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j \in ℤ$
26	25	zcnd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j \in ℂ$
27	26 11	npcand	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j - M + M = j$
28	27	eqcomd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to j = j - M + M$
29	20 23 28	rspcedvd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to \exists i \in (0 ..^N - M) j = i + M$
30		eqcom	$⊢ y = W (j) \leftrightarrow W (j) = y$
31		simpr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j = i + M) \to j = i + M$
32	31	fveq2d	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j = i + M) \to W (j) = W (i + M)$
33	32	eqeq2d	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j = i + M) \to (y = W (j) \leftrightarrow y = W (i + M))$
34	30 33	bitr3id	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j = i + M) \to (W (j) = y \leftrightarrow y = W (i + M))$
35	7 29 34	rexxfrd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (\exists j \in (M ..^N) W (j) = y \leftrightarrow \exists i \in (0 ..^N - M) y = W (i + M))$
36		eqid	$⊢ (i \in (0 ..^N - M) ⟼ W (i + M)) = (i \in (0 ..^N - M) ⟼ W (i + M))$
37		fvex	$⊢ W (i + M) \in V$
38	36 37	elrnmpti	$⊢ y \in ran (i \in (0 ..^N - M) ⟼ W (i + M)) \leftrightarrow \exists i \in (0 ..^N - M) y = W (i + M)$
39	35 38	bitr4di	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (\exists j \in (M ..^N) W (j) = y \leftrightarrow y \in ran (i \in (0 ..^N - M) ⟼ W (i + M)))$
40		wrdf	$⊢ W \in Word V \to W : (0 ..^\|W\|) ⟶ V$
41	40	3ad2ant1	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W : (0 ..^\|W\|) ⟶ V$
42	41	ffnd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W Fn (0 ..^\|W\|)$
43		elfzuz	$⊢ M \in (0 \dots N) \to M \in ℤ_{\geq 0}$
44	43	3ad2ant2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to M \in ℤ_{\geq 0}$
45		fzoss1	$⊢ M \in ℤ_{\geq 0} \to (M ..^N) \subseteq (0 ..^N)$
46	44 45	syl	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (M ..^N) \subseteq (0 ..^N)$
47		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
48	47	3ad2ant3	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \|W\| \in ℤ_{\geq N}$
49		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
50	48 49	syl	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (0 ..^N) \subseteq (0 ..^\|W\|)$
51	46 50	sstrd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (M ..^N) \subseteq (0 ..^\|W\|)$
52	42 51	fvelimabd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (y \in W [(M ..^N)] \leftrightarrow \exists j \in (M ..^N) W (j) = y)$
53		swrdval2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W substr ⟨M, N⟩ = (i \in (0 ..^N - M) ⟼ W (i + M))$
54	53	rneqd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) = ran (i \in (0 ..^N - M) ⟼ W (i + M))$
55	54	eleq2d	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (y \in ran (W substr ⟨M, N⟩) \leftrightarrow y \in ran (i \in (0 ..^N - M) ⟼ W (i + M)))$
56	39 52 55	3bitr4rd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (y \in ran (W substr ⟨M, N⟩) \leftrightarrow y \in W [(M ..^N)])$
57	56	eqrdv	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) = W [(M ..^N)]$

Metamath Proof Explorer

Theorem swrdrn3

Proof