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		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\|)$
19	18	elfzelzd	$⊢ ((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 ℤ$
20		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)$
21	20	elfzelzd	$⊢ ((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 ℤ$
22		fzoaddel2	$⊢ (x \in (0 ..^N - M) \land N \in ℤ \land M \in ℤ) \to x + M \in (M ..^N)$
23	17 19 21 22	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)$
24	16 23	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)$
25	11 24	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\|)$
26		wrddm	$⊢ W \in Word V \to dom W = (0 ..^\|W\|)$
27	26	3ad2ant1	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to dom W = (0 ..^\|W\|)$
28	27	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\|)$
29	25 28	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$
30		fvelrn	$⊢ (Fun W \land x + M \in dom W) \to W (x + M) \in ran W$
31	6 29 30	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$
32	31	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$
33		eqid	$⊢ (x \in (0 ..^N - M) ⟼ W (x + M)) = (x \in (0 ..^N - M) ⟼ W (x + M))$
34	33	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$
35	32 34	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$
36	2 35	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