swrdcl

Description: Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	swrdcl	$⊢ S \in Word A \to S substr ⟨F, L⟩ \in Word A$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ S substr ⟨F, L⟩ = \emptyset \to (S substr ⟨F, L⟩ \in Word A \leftrightarrow \emptyset \in Word A)$
2		n0	$⊢ S substr ⟨F, L⟩ \neq \emptyset \leftrightarrow \exists x x \in (S substr ⟨F, L⟩)$
3		df-substr	$⊢ substr = (s \in V, b \in (ℤ \times ℤ) ⟼ if ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s, (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))), \emptyset))$
4	3	elmpocl2	$⊢ x \in (S substr ⟨F, L⟩) \to ⟨F, L⟩ \in (ℤ \times ℤ)$
5		opelxp	$⊢ ⟨F, L⟩ \in (ℤ \times ℤ) \leftrightarrow (F \in ℤ \land L \in ℤ)$
6	4 5	sylib	$⊢ x \in (S substr ⟨F, L⟩) \to (F \in ℤ \land L \in ℤ)$
7	6	exlimiv	$⊢ \exists x x \in (S substr ⟨F, L⟩) \to (F \in ℤ \land L \in ℤ)$
8	2 7	sylbi	$⊢ S substr ⟨F, L⟩ \neq \emptyset \to (F \in ℤ \land L \in ℤ)$
9		swrdval	$⊢ (S \in Word A \land F \in ℤ \land L \in ℤ) \to S substr ⟨F, L⟩ = if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset)$
10		wrdf	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ A$
11	10	3ad2ant1	$⊢ (S \in Word A \land F \in ℤ \land L \in ℤ) \to S : (0 ..^\|S\|) ⟶ A$
12	11	ad2antrr	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to S : (0 ..^\|S\|) ⟶ A$
13		simplr	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to (F ..^L) \subseteq dom S$
14		simpr	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to x \in (0 ..^L - F)$
15		simpll3	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to L \in ℤ$
16		simpll2	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to F \in ℤ$
17		fzoaddel2	$⊢ (x \in (0 ..^L - F) \land L \in ℤ \land F \in ℤ) \to x + F \in (F ..^L)$
18	14 15 16 17	syl3anc	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to x + F \in (F ..^L)$
19	13 18	sseldd	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to x + F \in dom S$
20	12	fdmd	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to dom S = (0 ..^\|S\|)$
21	19 20	eleqtrd	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to x + F \in (0 ..^\|S\|)$
22	12 21	ffvelrnd	$⊢ (((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \land x \in (0 ..^L - F)) \to S (x + F) \in A$
23	22	fmpttd	$⊢ ((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \to (x \in (0 ..^L - F) ⟼ S (x + F)) : (0 ..^L - F) ⟶ A$
24		iswrdi	$⊢ (x \in (0 ..^L - F) ⟼ S (x + F)) : (0 ..^L - F) ⟶ A \to (x \in (0 ..^L - F) ⟼ S (x + F)) \in Word A$
25	23 24	syl	$⊢ ((S \in Word A \land F \in ℤ \land L \in ℤ) \land (F ..^L) \subseteq dom S) \to (x \in (0 ..^L - F) ⟼ S (x + F)) \in Word A$
26		wrd0	$⊢ \emptyset \in Word A$
27	26	a1i	$⊢ ((S \in Word A \land F \in ℤ \land L \in ℤ) \land \neg (F ..^L) \subseteq dom S) \to \emptyset \in Word A$
28	25 27	ifclda	$⊢ (S \in Word A \land F \in ℤ \land L \in ℤ) \to if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset) \in Word A$
29	9 28	eqeltrd	$⊢ (S \in Word A \land F \in ℤ \land L \in ℤ) \to S substr ⟨F, L⟩ \in Word A$
30	29	3expb	$⊢ (S \in Word A \land (F \in ℤ \land L \in ℤ)) \to S substr ⟨F, L⟩ \in Word A$
31	8 30	sylan2	$⊢ (S \in Word A \land S substr ⟨F, L⟩ \neq \emptyset) \to S substr ⟨F, L⟩ \in Word A$
32	26	a1i	$⊢ S \in Word A \to \emptyset \in Word A$
33	1 31 32	pm2.61ne	$⊢ S \in Word A \to S substr ⟨F, L⟩ \in Word A$

Metamath Proof Explorer

Theorem swrdcl

Proof