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

Definition df-splice 13102
Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-splice splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)))
Distinct variable group:   𝑠,𝑏

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 13094 . 2 class splice
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3169 . . 3 class V
52cv 1473 . . . . . 6 class 𝑠
6 cc0 9789 . . . . . . 7 class 0
73cv 1473 . . . . . . . . 9 class 𝑏
8 c1st 7031 . . . . . . . . 9 class 1st
97, 8cfv 5787 . . . . . . . 8 class (1st𝑏)
109, 8cfv 5787 . . . . . . 7 class (1st ‘(1st𝑏))
116, 10cop 4127 . . . . . 6 class ⟨0, (1st ‘(1st𝑏))⟩
12 csubstr 13093 . . . . . 6 class substr
135, 11, 12co 6524 . . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩)
14 c2nd 7032 . . . . . 6 class 2nd
157, 14cfv 5787 . . . . 5 class (2nd𝑏)
16 cconcat 13091 . . . . 5 class ++
1713, 15, 16co 6524 . . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏))
189, 14cfv 5787 . . . . . 6 class (2nd ‘(1st𝑏))
19 chash 12931 . . . . . . 7 class #
205, 19cfv 5787 . . . . . 6 class (#‘𝑠)
2118, 20cop 4127 . . . . 5 class ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩
225, 21, 12co 6524 . . . 4 class (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)
2317, 22, 16co 6524 . . 3 class (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩))
242, 3, 4, 4, 23cmpt2 6526 . 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)))
251, 24wceq 1474 1 wff splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  splval  13296  splcl  13297
  Copyright terms: Public domain W3C validator