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

Definition df-splice 12501
Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-splice  |- splice  =  ( s  e.  _V , 
b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. ) ++  ( 2nd `  b ) ) ++  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Distinct variable group:    s, b

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 12493 . 2  class splice
2 vs . . 3  setvar  s
3 vb . . 3  setvar  b
4 cvv 3056 . . 3  class  _V
52cv 1402 . . . . . 6  class  s
6 cc0 9440 . . . . . . 7  class  0
73cv 1402 . . . . . . . . 9  class  b
8 c1st 6734 . . . . . . . . 9  class  1st
97, 8cfv 5523 . . . . . . . 8  class  ( 1st `  b )
109, 8cfv 5523 . . . . . . 7  class  ( 1st `  ( 1st `  b
) )
116, 10cop 3975 . . . . . 6  class  <. 0 ,  ( 1st `  ( 1st `  b ) )
>.
12 csubstr 12492 . . . . . 6  class substr
135, 11, 12co 6232 . . . . 5  class  ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. )
14 c2nd 6735 . . . . . 6  class  2nd
157, 14cfv 5523 . . . . 5  class  ( 2nd `  b )
16 cconcat 12490 . . . . 5  class ++
1713, 15, 16co 6232 . . . 4  class  ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) ) >.
) ++  ( 2nd `  b
) )
189, 14cfv 5523 . . . . . 6  class  ( 2nd `  ( 1st `  b
) )
19 chash 12357 . . . . . . 7  class  #
205, 19cfv 5523 . . . . . 6  class  ( # `  s )
2118, 20cop 3975 . . . . 5  class  <. ( 2nd `  ( 1st `  b
) ) ,  (
# `  s ) >.
225, 21, 12co 6232 . . . 4  class  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. )
2317, 22, 16co 6232 . . 3  class  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) ++  ( 2nd `  b ) ) ++  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) )
242, 3, 4, 4, 23cmpt2 6234 . 2  class  ( s  e.  _V ,  b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) ++  ( 2nd `  b ) ) ++  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
251, 24wceq 1403 1  wff splice  =  ( s  e.  _V , 
b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. ) ++  ( 2nd `  b ) ) ++  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  splval  12688  splcl  12689
  Copyright terms: Public domain W3C validator