Metamath Proof Explorer

Definition 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 ∈ V , b ∈ ℤ × ℤ ⟼ if 1 st ⁡ b ..^ 2 nd ⁡ b ⊆ dom ⁡ s x ∈ 0 ..^ 2 nd ⁡ b − 1 st ⁡ b ⟼ s ⁡ x + 1 st ⁡ b ∅

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 ℤ × ℤ
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 ⊆ 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 ∈ 0 ..^ 2 nd ⁡ b − 1 st ⁡ b ⟼ s ⁡ x + 1 st ⁡ b
26 c0 class ∅
27 15 25 26 cif class if 1 st ⁡ b ..^ 2 nd ⁡ b ⊆ dom ⁡ s x ∈ 0 ..^ 2 nd ⁡ b − 1 st ⁡ b ⟼ s ⁡ x + 1 st ⁡ b ∅
28 1 3 2 5 27 cmpo class s ∈ V , b ∈ ℤ × ℤ ⟼ if 1 st ⁡ b ..^ 2 nd ⁡ b ⊆ dom ⁡ s x ∈ 0 ..^ 2 nd ⁡ b − 1 st ⁡ b ⟼ s ⁡ x + 1 st ⁡ b ∅
29 0 28 wceq wff substr = s ∈ V , b ∈ ℤ × ℤ ⟼ if 1 st ⁡ b ..^ 2 nd ⁡ b ⊆ dom ⁡ s x ∈ 0 ..^ 2 nd ⁡ b − 1 st ⁡ b ⟼ s ⁡ x + 1 st ⁡ b ∅