splval

Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 11-May-2020) (Revised by AV, 15-Oct-2022)

		Ref	Expression
	Assertion	splval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-splice	⊢ splice = ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) )
2	1	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → splice = ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) ) )
3		simprl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → 𝑠 = 𝑆 )
4		2fveq3	⊢ ( 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
5	4	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
6		ot1stg	⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = 𝐹 )
7	6	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = 𝐹 )
8	5 7	sylan9eqr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) = 𝐹 )
9	3 8	oveq12d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) = ( 𝑆 prefix 𝐹 ) )
10		fveq2	⊢ ( 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) )
11	10	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) )
12		ot3rdg	⊢ ( 𝑅 ∈ 𝑌 → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = 𝑅 )
13	12	3ad2ant3	⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = 𝑅 )
14	13	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = 𝑅 )
15	11 14	sylan9eqr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( 2^nd ‘ 𝑏 ) = 𝑅 )
16	9 15	oveq12d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) = ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) )
17		2fveq3	⊢ ( 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
18	17	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
19		ot2ndg	⊢ ( ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = 𝑇 )
20	19	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = 𝑇 )
21	18 20	sylan9eqr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) = 𝑇 )
22	3	fveq2d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑆 ) )
23	21 22	opeq12d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ = ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ )
24	3 23	oveq12d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) = ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) )
25	16 24	oveq12d	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) → ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
26		elex	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
27	26	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → 𝑆 ∈ V )
28		otex	⊢ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ∈ V
29	28	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ∈ V )
30		ovexd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ∈ V )
31	2 25 27 29 30	ovmpod	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )

Metamath Proof Explorer

Theorem splval

Proof