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 14391

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 14390	. 2 class splice
2		vs	. . 3 setvar 𝑠
3		vb	. . 3 setvar 𝑏
4		cvv 3422	. . 3 class V
5	2	cv 1538	. . . . . 6 class 𝑠
6	3	cv 1538	. . . . . . . 8 class 𝑏
7		c1st 7802	. . . . . . . 8 class 1^st
8	6, 7	cfv 6418	. . . . . . 7 class (1^st ‘𝑏)
9	8, 7	cfv 6418	. . . . . 6 class (1^st ‘(1^st ‘𝑏))
10		cpfx 14311	. . . . . 6 class prefix
11	5, 9, 10	co 7255	. . . . 5 class (𝑠 prefix (1^st ‘(1^st ‘𝑏)))
12		c2nd 7803	. . . . . 6 class 2^nd
13	6, 12	cfv 6418	. . . . 5 class (2^nd ‘𝑏)
14		cconcat 14201	. . . . 5 class ++
15	11, 13, 14	co 7255	. . . 4 class ((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏))
16	8, 12	cfv 6418	. . . . . 6 class (2^nd ‘(1^st ‘𝑏))
17		chash 13972	. . . . . . 7 class ♯
18	5, 17	cfv 6418	. . . . . 6 class (♯‘𝑠)
19	16, 18	cop 4564	. . . . 5 class ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩
20		csubstr 14281	. . . . 5 class substr
21	5, 19, 20	co 7255	. . . 4 class (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)
22	15, 21, 14	co 7255	. . 3 class (((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩))
23	2, 3, 4, 4, 22	cmpo 7257	. 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1^st ‘(1^st ‘𝑏))) ++ (2^nd ‘𝑏)) ++ (𝑠 substr ⟨(2^nd ‘(1^st ‘𝑏)), (♯‘𝑠)⟩)))
24	1, 23	wceq 1539	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 14392 splcl 14393