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

Definition df-splice 13259
 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 13251 . 2 class splice
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3190 . . 3 class V
52cv 1479 . . . . . 6 class 𝑠
6 cc0 9896 . . . . . . 7 class 0
73cv 1479 . . . . . . . . 9 class 𝑏
8 c1st 7126 . . . . . . . . 9 class 1st
97, 8cfv 5857 . . . . . . . 8 class (1st𝑏)
109, 8cfv 5857 . . . . . . 7 class (1st ‘(1st𝑏))
116, 10cop 4161 . . . . . 6 class ⟨0, (1st ‘(1st𝑏))⟩
12 csubstr 13250 . . . . . 6 class substr
135, 11, 12co 6615 . . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩)
14 c2nd 7127 . . . . . 6 class 2nd
157, 14cfv 5857 . . . . 5 class (2nd𝑏)
16 cconcat 13248 . . . . 5 class ++
1713, 15, 16co 6615 . . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏))
189, 14cfv 5857 . . . . . 6 class (2nd ‘(1st𝑏))
19 chash 13073 . . . . . . 7 class #
205, 19cfv 5857 . . . . . 6 class (#‘𝑠)
2118, 20cop 4161 . . . . 5 class ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩
225, 21, 12co 6615 . . . 4 class (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)
2317, 22, 16co 6615 . . 3 class (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩))
242, 3, 4, 4, 23cmpt2 6617 . 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)))
251, 24wceq 1480 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  13455  splcl  13456
 Copyright terms: Public domain W3C validator