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

Definition df-splice 12226
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
) ) >. ) concat  ( 2nd `  b ) ) concat  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Distinct variable group:    s, b

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 12218 . 2  class splice
2 vs . . 3  setvar  s
3 vb . . 3  setvar  b
4 cvv 2967 . . 3  class  _V
52cv 1368 . . . . . 6  class  s
6 cc0 9274 . . . . . . 7  class  0
73cv 1368 . . . . . . . . 9  class  b
8 c1st 6570 . . . . . . . . 9  class  1st
97, 8cfv 5413 . . . . . . . 8  class  ( 1st `  b )
109, 8cfv 5413 . . . . . . 7  class  ( 1st `  ( 1st `  b
) )
116, 10cop 3878 . . . . . 6  class  <. 0 ,  ( 1st `  ( 1st `  b ) )
>.
12 csubstr 12217 . . . . . 6  class substr
135, 11, 12co 6086 . . . . 5  class  ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. )
14 c2nd 6571 . . . . . 6  class  2nd
157, 14cfv 5413 . . . . 5  class  ( 2nd `  b )
16 cconcat 12215 . . . . 5  class concat
1713, 15, 16co 6086 . . . 4  class  ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) ) >.
) concat  ( 2nd `  b
) )
189, 14cfv 5413 . . . . . 6  class  ( 2nd `  ( 1st `  b
) )
19 chash 12095 . . . . . . 7  class  #
205, 19cfv 5413 . . . . . 6  class  ( # `  s )
2118, 20cop 3878 . . . . 5  class  <. ( 2nd `  ( 1st `  b
) ) ,  (
# `  s ) >.
225, 21, 12co 6086 . . . 4  class  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. )
2317, 22, 16co 6086 . . 3  class  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) concat  ( 2nd `  b
) ) concat  ( s substr  <.
( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) )
242, 3, 4, 4, 23cmpt2 6088 . 2  class  ( s  e.  _V ,  b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) concat  ( 2nd `  b
) ) concat  ( s substr  <.
( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
251, 24wceq 1369 1  wff splice  =  ( s  e.  _V , 
b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. ) concat  ( 2nd `  b ) ) concat  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  splval  12385  splcl  12386
  Copyright terms: Public domain W3C validator