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

Definition df-spliceOLD 13888
 Description: Obsolete version of df-splice 13887 as of 12-Oct-2022. Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (New usage is discouraged.)
Assertion
Ref Expression
df-spliceOLD spliceOLD = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
Distinct variable group:   𝑠,𝑏

Detailed syntax breakdown of Definition df-spliceOLD
StepHypRef Expression
1 cspliceOLD 13886 . 2 class spliceOLD
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3397 . . 3 class V
52cv 1600 . . . . . 6 class 𝑠
6 cc0 10272 . . . . . . 7 class 0
73cv 1600 . . . . . . . . 9 class 𝑏
8 c1st 7443 . . . . . . . . 9 class 1st
97, 8cfv 6135 . . . . . . . 8 class (1st𝑏)
109, 8cfv 6135 . . . . . . 7 class (1st ‘(1st𝑏))
116, 10cop 4403 . . . . . 6 class ⟨0, (1st ‘(1st𝑏))⟩
12 csubstr 13730 . . . . . 6 class substr
135, 11, 12co 6922 . . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩)
14 c2nd 7444 . . . . . 6 class 2nd
157, 14cfv 6135 . . . . 5 class (2nd𝑏)
16 cconcat 13660 . . . . 5 class ++
1713, 15, 16co 6922 . . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏))
189, 14cfv 6135 . . . . . 6 class (2nd ‘(1st𝑏))
19 chash 13435 . . . . . . 7 class
205, 19cfv 6135 . . . . . 6 class (♯‘𝑠)
2118, 20cop 4403 . . . . 5 class ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩
225, 21, 12co 6922 . . . 4 class (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)
2317, 22, 16co 6922 . . 3 class (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩))
242, 3, 4, 4, 23cmpt2 6924 . 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
251, 24wceq 1601 1 wff spliceOLD = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
 Colors of variables: wff setvar class This definition is referenced by:  splvalpfxOLD  13889  splvalOLD  13891  splclOLD  13893
 Copyright terms: Public domain W3C validator