swrdrn2

Description: The range of a subword is a subset of the range of that word. Stronger version of swrdrn . (Contributed by Thierry Arnoux, 12-Dec-2023)

		Ref	Expression
	Assertion	swrdrn2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) \subseteq ran W$

Proof

Step	Hyp	Ref	Expression
1		swrdval2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to W substr ⟨M, N⟩ = (x \in (0 ..^N - M) ⟼ W (x + M))$
2	1	rneqd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) = ran (x \in (0 ..^N - M) ⟼ W (x + M))$
3		eqidd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to \|W\| = \|W\|$
4		simpl1	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to W \in Word V$
5	3 4	wrdfd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to W : (0 ..^\|W\|) ⟶ V$
6	5	ffund	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to Fun W$
7		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
8	7	3ad2ant3	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \|W\| \in ℤ_{\geq N}$
9	8	adantr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to \|W\| \in ℤ_{\geq N}$
10		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
11	9 10	syl	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to (0 ..^N) \subseteq (0 ..^\|W\|)$
12		elfzuz	$⊢ M \in (0 \dots N) \to M \in ℤ_{\geq 0}$
13	12	3ad2ant2	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to M \in ℤ_{\geq 0}$
14	13	adantr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to M \in ℤ_{\geq 0}$
15		fzoss1	$⊢ M \in ℤ_{\geq 0} \to (M ..^N) \subseteq (0 ..^N)$
16	14 15	syl	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to (M ..^N) \subseteq (0 ..^N)$
17		simpr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to x \in (0 ..^N - M)$
18		fzssz	$⊢ (0 \dots \|W\|) \subseteq ℤ$
19		simpl3	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to N \in (0 \dots \|W\|)$
20	18 19	sseldi	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to N \in ℤ$
21		fzssz	$⊢ (0 \dots N) \subseteq ℤ$
22		simpl2	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to M \in (0 \dots N)$
23	21 22	sseldi	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to M \in ℤ$
24		fzoaddel2	$⊢ (x \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to x + M \in (M ..^N)$
25	17 20 23 24	syl3anc	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to x + M \in (M ..^N)$
26	16 25	sseldd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to x + M \in (0 ..^N)$
27	11 26	sseldd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to x + M \in (0 ..^\|W\|)$
28		wrddm	$⊢ W \in Word V \to dom W = (0 ..^\|W\|)$
29	28	3ad2ant1	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to dom W = (0 ..^\|W\|)$
30	29	adantr	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to dom W = (0 ..^\|W\|)$
31	27 30	eleqtrrd	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to x + M \in dom W$
32		fvelrn	$⊢ (Fun W \land x + M \in dom W) \to W (x + M) \in ran W$
33	6 31 32	syl2anc	$⊢ ((W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \land x \in (0 ..^N - M)) \to W (x + M) \in ran W$
34	33	ralrimiva	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to \forall x \in (0 ..^N - M) W (x + M) \in ran W$
35		eqid	$⊢ (x \in (0 ..^N - M) ⟼ W (x + M)) = (x \in (0 ..^N - M) ⟼ W (x + M))$
36	35	rnmptss	$⊢ \forall x \in (0 ..^N - M) W (x + M) \in ran W \to ran (x \in (0 ..^N - M) ⟼ W (x + M)) \subseteq ran W$
37	34 36	syl	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (x \in (0 ..^N - M) ⟼ W (x + M)) \subseteq ran W$
38	2 37	eqsstrd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) \subseteq ran W$

Metamath Proof Explorer

Theorem swrdrn2

Proof