Metamath Proof Explorer

Definition df-splice

Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 14-Oct-2022)

Ref Expression
Assertion df-splice 
|- splice = ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csplice 
 |-  splice
1 vs 
 |-  s
2 cvv 
 |-  _V
3 vb 
 |-  b
4 1 cv 
 |-  s
5 cpfx 
 |-  prefix
6 c1st 
 |-  1st
7 3 cv 
 |-  b
8 7 6 cfv 
 |-  ( 1st ` b )
9 8 6 cfv 
 |-  ( 1st ` ( 1st ` b ) )
10 4 9 5 co 
 |-  ( s prefix ( 1st ` ( 1st ` b ) ) )
11 cconcat 
 |-  ++
12 c2nd 
 |-  2nd
13 7 12 cfv 
 |-  ( 2nd ` b )
14 10 13 11 co 
 |-  ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) )
15 csubstr 
 |-  substr
16 8 12 cfv 
 |-  ( 2nd ` ( 1st ` b ) )
17 chash 
 |-  #
18 4 17 cfv 
 |-  ( # ` s )
19 16 18 cop 
 |-  <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >.
20 4 19 15 co 
 |-  ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. )
21 14 20 11 co 
 |-  ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) )
22 1 3 2 2 21 cmpo 
 |-  ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )
23 0 22 wceq 
 |-  splice = ( s e. _V , b e. _V |-> ( ( ( s prefix ( 1st ` ( 1st ` b ) ) ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )