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		fzssz	$⊢ (0 \dots \|W\|) \subseteq ℤ$
3		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\|)$
4	2 3	sseldi	$⊢ ((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 ℤ$
5		fzssz	$⊢ (0 \dots N) \subseteq ℤ$
6		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)$
7	5 6	sseldi	$⊢ ((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 ℤ$
8		fzoaddel2	$⊢ (i \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to i + M \in (M ..^N)$
9	1 4 7 8	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)$
10		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)$
11		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)$
12	5 11	sseldi	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to M \in ℤ$
13	12	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 ℂ$
14		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\|)$
15	2 14	sseldi	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land j \in (M ..^N)) \to N \in ℤ$
16	15	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 ℂ$
17	13 16	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$
18	17	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)$
19	10 18	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)$
20	15 12	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 ℤ$
21		fzosubel3	$⊢ (j \in (M ..^M + N - M) \land N - M \in ℤ) \to j - M \in (0 ..^N - M)$
22	19 20 21	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)$
23		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$
24	23	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$
25	24	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)$
26		fzossz	$⊢ (M ..^N) \subseteq ℤ$
27	26 10	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 ℤ$
28	27	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 ℂ$
29	28 13	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$
30	29	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$
31	22 25 30	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$
32		eqcom	$⊢ y = W (j) \leftrightarrow W (j) = y$
33		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$
34	33	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)$
35	34	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))$
36	32 35	syl5bbr	$⊢ ((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))$
37	9 31 36	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))$
38		eqid	$⊢ (i \in (0 ..^N - M) ⟼ W (i + M)) = (i \in (0 ..^N - M) ⟼ W (i + M))$
39		fvex	$⊢ W (i + M) \in V$
40	38 39	elrnmpti	$⊢ y \in ran (i \in (0 ..^N - M) ⟼ W (i + M)) \leftrightarrow \exists i \in (0 ..^N - M) y = W (i + M)$
41	37 40	syl6bbr	$⊢ (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)))$
42		wrdf	$⊢ W \in Word V \to W : (0 ..^\|W\|) ⟶ V$
43	42	3ad2ant1	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W : (0 ..^\|W\|) ⟶ V$
44	43	ffnd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W Fn (0 ..^\|W\|)$
45		elfzuz	$⊢ M \in (0 \dots N) \to M \in ℤ_{\geq 0}$
46	45	3ad2ant2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to M \in ℤ_{\geq 0}$
47		fzoss1	$⊢ M \in ℤ_{\geq 0} \to (M ..^N) \subseteq (0 ..^N)$
48	46 47	syl	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (M ..^N) \subseteq (0 ..^N)$
49		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
50	49	3ad2ant3	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \|W\| \in ℤ_{\geq N}$
51		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
52	50 51	syl	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (0 ..^N) \subseteq (0 ..^\|W\|)$
53	48 52	sstrd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (M ..^N) \subseteq (0 ..^\|W\|)$
54	44 53	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)$
55		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))$
56	55	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))$
57	56	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)))$
58	41 54 57	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)])$
59	58	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