df-substr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-substr		Structured version Visualization version GIF version

Definition df-substr 14711

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

**Assertion**
Ref	Expression
df-substr	⊢ substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1^st ‘𝑏)..^(2^nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2^nd ‘𝑏) − (1^st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1^st ‘𝑏)))), ∅))

Distinct variable group: 𝑠,𝑏,𝑥

**Detailed syntax breakdown of Definition df-substr**
Step	Hyp	Ref	Expression
1		csubstr 14710	. 2 class substr
2		vs	. . 3 setvar 𝑠
3		vb	. . 3 setvar 𝑏
4		cvv 3453	. . 3 class V
5		cz 12618	. . . 4 class ℤ
6	5, 5	cxp 5657	. . 3 class (ℤ × ℤ)
7	3	cv 1569	. . . . . . 7 class 𝑏
8		c1st 7987	. . . . . . 7 class 1^st
9	7, 8	cfv 6537	. . . . . 6 class (1^st ‘𝑏)
10		c2nd 7988	. . . . . . 7 class 2^nd
11	7, 10	cfv 6537	. . . . . 6 class (2^nd ‘𝑏)
12		cfzo 13711	. . . . . 6 class ..^
13	9, 11, 12	co 7416	. . . . 5 class ((1^st ‘𝑏)..^(2^nd ‘𝑏))
14	2	cv 1569	. . . . . 6 class 𝑠
15	14	cdm 5659	. . . . 5 class dom 𝑠
16	13, 15	wss 3902	. . . 4 wff ((1^st ‘𝑏)..^(2^nd ‘𝑏)) ⊆ dom 𝑠
17		vx	. . . . 5 setvar 𝑥
18		cc0 11127	. . . . . 6 class 0
19		cmin 11468	. . . . . . 7 class −
20	11, 9, 19	co 7416	. . . . . 6 class ((2^nd ‘𝑏) − (1^st ‘𝑏))
21	18, 20, 12	co 7416	. . . . 5 class (0..^((2^nd ‘𝑏) − (1^st ‘𝑏)))
22	17	cv 1569	. . . . . . 7 class 𝑥
23		caddc 11130	. . . . . . 7 class +
24	22, 9, 23	co 7416	. . . . . 6 class (𝑥 + (1^st ‘𝑏))
25	24, 14	cfv 6537	. . . . 5 class (𝑠‘(𝑥 + (1^st ‘𝑏)))
26	17, 21, 25	cmpt 5190	. . . 4 class (𝑥 ∈ (0..^((2^nd ‘𝑏) − (1^st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1^st ‘𝑏))))
27		c0 4282	. . . 4 class ∅
28	16, 26, 27	cif 4485	. . 3 class if(((1^st ‘𝑏)..^(2^nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2^nd ‘𝑏) − (1^st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1^st ‘𝑏)))), ∅)
29	2, 3, 4, 6, 28	cmpo 7418	. 2 class (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1^st ‘𝑏)..^(2^nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2^nd ‘𝑏) − (1^st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1^st ‘𝑏)))), ∅))
30	1, 29	wceq 1570	1 wff substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1^st ‘𝑏)..^(2^nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2^nd ‘𝑏) − (1^st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1^st ‘𝑏)))), ∅))

Colors of variables: wff setvar class

This definition is used by: swrdnznd 14712 swrdval 14713 swrd00 14714 swrdcl 14715 swrd0 14730

W3C validator