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 13534
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 13526 . 2 class splice
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3402 . . 3 class V
52cv 1636 . . . . . 6 class 𝑠
6 cc0 10230 . . . . . . 7 class 0
73cv 1636 . . . . . . . . 9 class 𝑏
8 c1st 7405 . . . . . . . . 9 class 1st
97, 8cfv 6110 . . . . . . . 8 class (1st𝑏)
109, 8cfv 6110 . . . . . . 7 class (1st ‘(1st𝑏))
116, 10cop 4387 . . . . . 6 class ⟨0, (1st ‘(1st𝑏))⟩
12 csubstr 13525 . . . . . 6 class substr
135, 11, 12co 6883 . . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩)
14 c2nd 7406 . . . . . 6 class 2nd
157, 14cfv 6110 . . . . 5 class (2nd𝑏)
16 cconcat 13523 . . . . 5 class ++
1713, 15, 16co 6883 . . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏))
189, 14cfv 6110 . . . . . 6 class (2nd ‘(1st𝑏))
19 chash 13356 . . . . . . 7 class
205, 19cfv 6110 . . . . . 6 class (♯‘𝑠)
2118, 20cop 4387 . . . . 5 class ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩
225, 21, 12co 6883 . . . 4 class (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)
2317, 22, 16co 6883 . . 3 class (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩))
242, 3, 4, 4, 23cmpt2 6885 . 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
251, 24wceq 1637 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  13745  splcl  13746
  Copyright terms: Public domain W3C validator