swrdval

Description: Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	swrdval	$⊢ (S \in V \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)$

Proof

Step	Hyp	Ref	Expression
1		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))$
2	1	a1i	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to 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))$
3		simprl	$⊢ ((S \in V \land F \in ℤ \land L \in ℤ) \land (s = S \land b = ⟨F, L⟩)) \to s = S$
4		fveq2	$⊢ b = ⟨F, L⟩ \to 1^{st} (b) = 1^{st} (⟨F, L⟩)$
5	4	adantl	$⊢ (s = S \land b = ⟨F, L⟩) \to 1^{st} (b) = 1^{st} (⟨F, L⟩)$
6		op1stg	$⊢ (F \in ℤ \land L \in ℤ) \to 1^{st} (⟨F, L⟩) = F$
7	6	3adant1	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to 1^{st} (⟨F, L⟩) = F$
8	5 7	sylan9eqr	$⊢ ((S \in V \land F \in ℤ \land L \in ℤ) \land (s = S \land b = ⟨F, L⟩)) \to 1^{st} (b) = F$
9		fveq2	$⊢ b = ⟨F, L⟩ \to 2^{nd} (b) = 2^{nd} (⟨F, L⟩)$
10	9	adantl	$⊢ (s = S \land b = ⟨F, L⟩) \to 2^{nd} (b) = 2^{nd} (⟨F, L⟩)$
11		op2ndg	$⊢ (F \in ℤ \land L \in ℤ) \to 2^{nd} (⟨F, L⟩) = L$
12	11	3adant1	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to 2^{nd} (⟨F, L⟩) = L$
13	10 12	sylan9eqr	$⊢ ((S \in V \land F \in ℤ \land L \in ℤ) \land (s = S \land b = ⟨F, L⟩)) \to 2^{nd} (b) = L$
14		simp2	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to 1^{st} (b) = F$
15		simp3	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to 2^{nd} (b) = L$
16	14 15	oveq12d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to (1^{st} (b) ..^2^{nd} (b)) = (F ..^L)$
17		simp1	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to s = S$
18	17	dmeqd	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to dom s = dom S$
19	16 18	sseq12d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to ((1^{st} (b) ..^2^{nd} (b)) \subseteq dom s \leftrightarrow (F ..^L) \subseteq dom S)$
20	15 14	oveq12d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to 2^{nd} (b) - 1^{st} (b) = L - F$
21	20	oveq2d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to (0 ..^2^{nd} (b) - 1^{st} (b)) = (0 ..^L - F)$
22	14	oveq2d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to x + 1^{st} (b) = x + F$
23	17 22	fveq12d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to s (x + 1^{st} (b)) = S (x + F)$
24	21 23	mpteq12dv	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b))) = (x \in (0 ..^L - F) ⟼ S (x + F))$
25	19 24	ifbieq1d	$⊢ (s = S \land 1^{st} (b) = F \land 2^{nd} (b) = L) \to 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) = if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset)$
26	3 8 13 25	syl3anc	$⊢ ((S \in V \land F \in ℤ \land L \in ℤ) \land (s = S \land b = ⟨F, L⟩)) \to 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) = if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset)$
27		elex	$⊢ S \in V \to S \in V$
28	27	3ad2ant1	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to S \in V$
29		opelxpi	$⊢ (F \in ℤ \land L \in ℤ) \to ⟨F, L⟩ \in (ℤ \times ℤ)$
30	29	3adant1	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to ⟨F, L⟩ \in (ℤ \times ℤ)$
31		ovex	$⊢ (0 ..^L - F) \in V$
32	31	mptex	$⊢ (x \in (0 ..^L - F) ⟼ S (x + F)) \in V$
33		0ex	$⊢ \emptyset \in V$
34	32 33	ifex	$⊢ if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset) \in V$
35	34	a1i	$⊢ (S \in V \land F \in ℤ \land L \in ℤ) \to if ((F ..^L) \subseteq dom S, (x \in (0 ..^L - F) ⟼ S (x + F)), \emptyset) \in V$
36	2 26 28 30 35	ovmpod	$⊢ (S \in V \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)$

Metamath Proof Explorer

Theorem swrdval

Proof