Definition df-splice 13159

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

Step	Hyp	Ref	Expression
1		csplice 13151	. 2 class splice
2		vs	. . 3 setvar 𝑠
3		vb	. . 3 setvar 𝑏
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . . . 6 class 𝑠
6		cc0 9815	. . . . . . 7 class 0
7	3	cv 1474	. . . . . . . . 9 class 𝑏
8		c1st 7057	. . . . . . . . 9 class 1st
9	7, 8	cfv 5804	. . . . . . . 8 class (1st ‘𝑏)
10	9, 8	cfv 5804	. . . . . . 7 class (1st ‘(1st ‘𝑏))
11	6, 10	cop 4131	. . . . . 6 class ⟨0, (1st ‘(1st ‘𝑏))⟩
12		csubstr 13150	. . . . . 6 class substr
13	5, 11, 12	co 6549	. . . . 5 class (𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩)
14		c2nd 7058	. . . . . 6 class 2nd
15	7, 14	cfv 5804	. . . . 5 class (2nd ‘𝑏)
16		cconcat 13148	. . . . 5 class ++
17	13, 15, 16	co 6549	. . . 4 class ((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏))
18	9, 14	cfv 5804	. . . . . 6 class (2nd ‘(1st ‘𝑏))
19		chash 12979	. . . . . . 7 class #
20	5, 19	cfv 5804	. . . . . 6 class (#‘𝑠)
21	18, 20	cop 4131	. . . . 5 class ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩
22	5, 21, 12	co 6549	. . . 4 class (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩)
23	17, 22, 16	co 6549	. . 3 class (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩))
24	2, 3, 4, 4, 23	cmpt2 6551	. 2 class (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩)))
25	1, 24	wceq 1475	1 wff splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩)))

This definition is referenced by:  splval  13353  splcl  13354