splcl

Description: Closure of the substring replacement operator. (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

		Ref	Expression
	Assertion	splcl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ∈ Word 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 ∈ V )
2		otex	⊢ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ∈ V
3		id	⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
4		2fveq3	⊢ ( 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
5	3 4	oveqan12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) = ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) )
6		simpr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ )
7	6	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) )
8	5 7	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) = ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
9		simpl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → 𝑠 = 𝑆 )
10	6	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) )
11	10	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) )
12	9	fveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑆 ) )
13	11 12	opeq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ = ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ )
14	9 13	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) = ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) )
15	8 14	oveq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑏 = ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) → ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) = ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
16		df-splice	⊢ splice = ( 𝑠 ∈ V , 𝑏 ∈ V ↦ ( ( ( 𝑠 prefix ( 1^st ‘ ( 1^st ‘ 𝑏 ) ) ) ++ ( 2^nd ‘ 𝑏 ) ) ++ ( 𝑠 substr ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑏 ) ) , ( ♯ ‘ 𝑠 ) ⟩ ) ) )
17		ovex	⊢ ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) ∈ V
18	15 16 17	ovmpoa	⊢ ( ( 𝑆 ∈ V ∧ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ∈ V ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
19	1 2 18	sylancl	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
20	19	adantr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
21		pfxcl	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ∈ Word 𝐴 )
22	21	adantr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ∈ Word 𝐴 )
23		ot3rdg	⊢ ( 𝑅 ∈ Word 𝐴 → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = 𝑅 )
24	23	adantl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = 𝑅 )
25		simpr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → 𝑅 ∈ Word 𝐴 )
26	24 25	eqeltrd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ∈ Word 𝐴 )
27		ccatcl	⊢ ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ∈ Word 𝐴 ∧ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ∈ Word 𝐴 ) → ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ∈ Word 𝐴 )
28	22 26 27	syl2anc	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ∈ Word 𝐴 )
29		swrdcl	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
30	29	adantr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
31		ccatcl	⊢ ( ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ) → ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) ∈ Word 𝐴 )
32	28 30 31	syl2anc	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ( ( 𝑆 prefix ( 1^st ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ) ++ ( 2^nd ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) ++ ( 𝑆 substr ⟨ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) , ( ♯ ‘ 𝑆 ) ⟩ ) ) ∈ Word 𝐴 )
33	20 32	eqeltrd	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ∈ Word 𝐴 )

Metamath Proof Explorer

Theorem splcl

Proof