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

Definition df-substr 12225
Description: Define an operation which extracts portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
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 ) ) ) ) ,  (/) ) )
Distinct variable group:    s, b, x

Detailed syntax breakdown of Definition df-substr
StepHypRef Expression
1 csubstr 12217 . 2  class substr
2 vs . . 3  setvar  s
3 vb . . 3  setvar  b
4 cvv 2967 . . 3  class  _V
5 cz 10638 . . . 4  class  ZZ
65, 5cxp 4833 . . 3  class  ( ZZ 
X.  ZZ )
73cv 1368 . . . . . . 7  class  b
8 c1st 6570 . . . . . . 7  class  1st
97, 8cfv 5413 . . . . . 6  class  ( 1st `  b )
10 c2nd 6571 . . . . . . 7  class  2nd
117, 10cfv 5413 . . . . . 6  class  ( 2nd `  b )
12 cfzo 11540 . . . . . 6  class ..^
139, 11, 12co 6086 . . . . 5  class  ( ( 1st `  b )..^ ( 2nd `  b
) )
142cv 1368 . . . . . 6  class  s
1514cdm 4835 . . . . 5  class  dom  s
1613, 15wss 3323 . . . 4  wff  ( ( 1st `  b )..^ ( 2nd `  b
) )  C_  dom  s
17 vx . . . . 5  setvar  x
18 cc0 9274 . . . . . 6  class  0
19 cmin 9587 . . . . . . 7  class  -
2011, 9, 19co 6086 . . . . . 6  class  ( ( 2nd `  b )  -  ( 1st `  b
) )
2118, 20, 12co 6086 . . . . 5  class  ( 0..^ ( ( 2nd `  b
)  -  ( 1st `  b ) ) )
2217cv 1368 . . . . . . 7  class  x
23 caddc 9277 . . . . . . 7  class  +
2422, 9, 23co 6086 . . . . . 6  class  ( x  +  ( 1st `  b
) )
2524, 14cfv 5413 . . . . 5  class  ( s `
 ( x  +  ( 1st `  b ) ) )
2617, 21, 25cmpt 4345 . . . 4  class  ( x  e.  ( 0..^ ( ( 2nd `  b
)  -  ( 1st `  b ) ) ) 
|->  ( s `  (
x  +  ( 1st `  b ) ) ) )
27 c0 3632 . . . 4  class  (/)
2816, 26, 27cif 3786 . . 3  class  if ( ( ( 1st `  b
)..^ ( 2nd `  b
) )  C_  dom  s ,  ( x  e.  ( 0..^ ( ( 2nd `  b )  -  ( 1st `  b
) ) )  |->  ( s `  ( x  +  ( 1st `  b
) ) ) ) ,  (/) )
292, 3, 4, 6, 28cmpt2 6088 . 2  class  ( 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
) ) ) ) ,  (/) ) )
301, 29wceq 1369 1  wff 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 ) ) ) ) ,  (/) ) )
Colors of variables: wff setvar class
This definition is referenced by:  swrdval  12305  swrd00  12306  swrdcl  12307  swrd0  12319
  Copyright terms: Public domain W3C validator