df-splice

Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 14-Oct-2022)

		Ref	Expression
	Assertion	df-splice	⊢ splice = ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) )

Step	Hyp	Ref	Expression
0		csplice	⊢ splice
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vb	⊢ 𝑏
4	1	cv	⊢ 𝑠
5		cpfx	⊢ prefix
6		c1st	⊢ 1^st
7	3	cv	⊢ 𝑏
8	7 6	cfv	⊢ ( 1^st ‘ 𝑏 )
9	8 6	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑏 ) )
10	4 9 5	co	⊢ ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) )
11		cconcat	⊢ ++
12		c2nd	⊢ 2^nd
13	7 12	cfv	⊢ ( 2^nd ‘ 𝑏 )
14	10 13 11	co	⊢ ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) )
15		csubstr	⊢ substr
16	8 12	cfv	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) )
17		chash	⊢ ♯
18	4 17	cfv	⊢ ( ♯ ‘ 𝑠 )
19	16 18	cop	⊢ ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩
20	4 19 15	co	⊢ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ )
21	14 20 11	co	⊢ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) )
22	1 3 2 2 21	cmpo	⊢ ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) )
23	0 22	wceq	⊢ splice = ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) )

Metamath Proof Explorer