df-splice - Metamath Proof Explorer

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

Definition df-splice 14539

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 (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)))

Distinct variable group: 𝑠,𝑏

**Detailed syntax breakdown of Definition df-splice**
Step	Hyp	Ref	Expression
1		csplice 14538	. 2 class splice
2		vs	. . 3 setvar 𝑠
3		vb	. . 3 setvar 𝑏
4		cvv 3440	. . 3 class V
5	2	cv 1539	. . . . . 6 class 𝑠
6	3	cv 1539	. . . . . . . 8 class 𝑏
7		c1st 7875	. . . . . . . 8 class 1^st
8	6, 7	cfv 6465	. . . . . . 7 class (1^st ‘𝑏)
9	8, 7	cfv 6465	. . . . . 6 class (1^st ‘(1^st ‘𝑏))
10		cpfx 14459	. . . . . 6 class prefix
11	5, 9, 10	co 7316	. . . . 5 class (𝑠 prefix (1^st ‘(1^st ‘𝑏)))
12		c2nd 7876	. . . . . 6 class 2^nd
13	6, 12	cfv 6465	. . . . 5 class (2^nd ‘𝑏)
14		cconcat 14351	. . . . 5 class ++
15	11, 13, 14	co 7316	. . . 4 class ((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏))
16	8, 12	cfv 6465	. . . . . 6 class (2^nd ‘(1^st ‘𝑏))
17		chash 14123	. . . . . . 7 class ♯
18	5, 17	cfv 6465	. . . . . 6 class (♯‘𝑠)
19	16, 18	cop 4576	. . . . 5 class ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩
20		csubstr 14429	. . . . 5 class substr
21	5, 19, 20	co 7316	. . . 4 class (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)
22	15, 21, 14	co 7316	. . 3 class (((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩))
23	2, 3, 4, 4, 22	cmpo 7318	. 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)))
24	1, 23	wceq 1540	1 wff splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)))

Colors of variables: wff setvar class

This definition is referenced by: splval 14540 splcl 14541