swrdval2

Description: Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 2-May-2020)

		Ref	Expression
	Assertion	swrdval2	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = (x \in (0 ..^L - F) ⟼ S (x + F))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S \in Word A$
2		elfzelz	$⊢ F \in (0 \dots L) \to F \in ℤ$
3	2	3ad2ant2	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to F \in ℤ$
4		elfzelz	$⊢ L \in (0 \dots \|S\|) \to L \in ℤ$
5	4	3ad2ant3	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to L \in ℤ$
6		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)$
7	1 3 5 6	syl3anc	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset)$
8		elfzuz	$⊢ F \in (0 \dots L) \to F \in ℤ_{\geq 0}$
9	8	3ad2ant2	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to F \in ℤ_{\geq 0}$
10		fzoss1	$⊢ F \in ℤ_{\geq 0} \to (F ..^L) \subseteq (0 ..^L)$
11	9 10	syl	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to (F ..^L) \subseteq (0 ..^L)$
12		elfzuz3	$⊢ L \in (0 \dots \|S\|) \to \|S\| \in ℤ_{\geq L}$
13	12	3ad2ant3	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to \|S\| \in ℤ_{\geq L}$
14		fzoss2	$⊢ \|S\| \in ℤ_{\geq L} \to (0 ..^L) \subseteq (0 ..^\|S\|)$
15	13 14	syl	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to (0 ..^L) \subseteq (0 ..^\|S\|)$
16	11 15	sstrd	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to (F ..^L) \subseteq (0 ..^\|S\|)$
17		wrddm	$⊢ S \in Word A \to dom S = (0 ..^\|S\|)$
18	17	3ad2ant1	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to dom S = (0 ..^\|S\|)$
19	16 18	sseqtrrd	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to (F ..^L) \subseteq dom S$
20	19	iftrued	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset) = (x \in (0 ..^L - F) ⟼ S (x + F))$
21	7 20	eqtrd	$⊢ (S \in Word A \land F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = (x \in (0 ..^L - F) ⟼ S (x + F))$

Metamath Proof Explorer

Theorem swrdval2

Proof