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 e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubstr 
 |-  substr
1 vs 
 |-  s
2 cvv 
 |-  _V
3 vb 
 |-  b
4 cz 
 |-  ZZ
5 4 4 cxp 
 |-  ( ZZ X. ZZ )
6 c1st 
 |-  1st
7 3 cv 
 |-  b
8 7 6 cfv 
 |-  ( 1st ` b )
9 cfzo 
 |-  ..^
10 c2nd 
 |-  2nd
11 7 10 cfv 
 |-  ( 2nd ` b )
12 8 11 9 co 
 |-  ( ( 1st ` b ) ..^ ( 2nd ` b ) )
13 1 cv 
 |-  s
14 13 cdm 
 |-  dom s
15 12 14 wss 
 |-  ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s
16 vx 
 |-  x
17 cc0 
 |-  0
18 cmin 
 |-  -
19 11 8 18 co 
 |-  ( ( 2nd ` b ) - ( 1st ` b ) )
20 17 19 9 co 
 |-  ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) )
21 16 cv 
 |-  x
22 caddc 
 |-  +
23 21 8 22 co 
 |-  ( x + ( 1st ` b ) )
24 23 13 cfv 
 |-  ( s ` ( x + ( 1st ` b ) ) )
25 16 20 24 cmpt 
 |-  ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) )
26 c0 
 |-  (/)
27 15 25 26 cif 
 |-  if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) )
28 1 3 2 5 27 cmpo 
 |-  ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
29 0 28 wceq 
 |-  substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )