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 14107
Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by AV, 14-Oct-2022.)
Assertion
Ref Expression
df-splice splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
Distinct variable group:   𝑠,𝑏

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 14106 . 2 class splice
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3444 . . 3 class V
52cv 1537 . . . . . 6 class 𝑠
63cv 1537 . . . . . . . 8 class 𝑏
7 c1st 7673 . . . . . . . 8 class 1st
86, 7cfv 6328 . . . . . . 7 class (1st𝑏)
98, 7cfv 6328 . . . . . 6 class (1st ‘(1st𝑏))
10 cpfx 14027 . . . . . 6 class prefix
115, 9, 10co 7139 . . . . 5 class (𝑠 prefix (1st ‘(1st𝑏)))
12 c2nd 7674 . . . . . 6 class 2nd
136, 12cfv 6328 . . . . 5 class (2nd𝑏)
14 cconcat 13917 . . . . 5 class ++
1511, 13, 14co 7139 . . . 4 class ((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏))
168, 12cfv 6328 . . . . . 6 class (2nd ‘(1st𝑏))
17 chash 13690 . . . . . . 7 class
185, 17cfv 6328 . . . . . 6 class (♯‘𝑠)
1916, 18cop 4534 . . . . 5 class ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩
20 csubstr 13997 . . . . 5 class substr
215, 19, 20co 7139 . . . 4 class (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)
2215, 21, 14co 7139 . . 3 class (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩))
232, 3, 4, 4, 22cmpo 7141 . 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
241, 23wceq 1538 1 wff splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  splval  14108  splcl  14109
  Copyright terms: Public domain W3C validator