df-substr

Description: Define an operation which extracts portions (calledsubwords or substrings) of words. Definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	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))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubstr	$class substr$
1		vs	$setvar s$
2		cvv	$class V$
3		vb	$setvar b$
4		cz	$class ℤ$
5	4 4	cxp	$class (ℤ \times ℤ)$
6		c1st	$class 1^{st}$
7	3	cv	$setvar b$
8	7 6	cfv	$class 1^{st} (b)$
9		cfzo	$class ..^$
10		c2nd	$class 2^{nd}$
11	7 10	cfv	$class 2^{nd} (b)$
12	8 11 9	co	$class (1^{st} (b) ..^2^{nd} (b))$
13	1	cv	$setvar s$
14	13	cdm	$class dom s$
15	12 14	wss	$wff (1^{st} (b) ..^2^{nd} (b)) \subseteq dom s$
16		vx	$setvar x$
17		cc0	$class 0$
18		cmin	$class -$
19	11 8 18	co	$class (2^{nd} (b) - 1^{st} (b))$
20	17 19 9	co	$class (0 ..^2^{nd} (b) - 1^{st} (b))$
21	16	cv	$setvar x$
22		caddc	$class +$
23	21 8 22	co	$class (x + 1^{st} (b))$
24	23 13	cfv	$class s (x + 1^{st} (b))$
25	16 20 24	cmpt	$class (x \in (0 ..^2^{nd} (b) - 1^{st} (b)) ⟼ s (x + 1^{st} (b)))$
26		c0	$class \emptyset$
27	15 25 26	cif	$class 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)$
28	1 3 2 5 27	cmpo	$class (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))$
29	0 28	wceq	$wff 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))$

Metamath Proof Explorer

Definition df-substr

Detailed syntax breakdown