Theorem splfv1

Description: Symbols to the left of a splice are unaffected. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

	Ref	Expression
Hypotheses	spllen.s	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
	spllen.f	⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
	spllen.t	⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
	spllen.r	⊢ ( 𝜑 → 𝑅 ∈ Word 𝐴 )
	splfv1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝐹 ) )
Assertion	splfv1	⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		spllen.s	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
2		spllen.f	⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
3		spllen.t	⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
4		spllen.r	⊢ ( 𝜑 → 𝑅 ∈ Word 𝐴 )
5		splfv1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝐹 ) )
6		splval	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑅 ∈ Word 𝐴 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
7	1 2 3 4 6	syl13anc	⊢ ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ 𝑋 ) = ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ 𝑋 ) )
9		pfxcl	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
10	1 9	syl	⊢ ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
11		ccatcl	⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
12	10 4 11	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
13		swrdcl	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
14	1 13	syl	⊢ ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
15	2	elfzelzd	⊢ ( 𝜑 → 𝐹 ∈ ℤ )
16	15	uzidd	⊢ ( 𝜑 → 𝐹 ∈ ( ℤ≥ ‘ 𝐹 ) )
17		lencl	⊢ ( 𝑅 ∈ Word 𝐴 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
18	4 17	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
19		uzaddcl	⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝑅 ) ∈ ℕ0 ) → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) )
20	16 18 19	syl2anc	⊢ ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) )
21		fzoss2	⊢ ( ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) → ( 0 ..^ 𝐹 ) ⊆ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
22	20 21	syl	⊢ ( 𝜑 → ( 0 ..^ 𝐹 ) ⊆ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
23	22 5	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
24		ccatlen	⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
25	10 4 24	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
26		fzass4	⊢ ( ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑇 ∈ ( 𝐹 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
27	26	biimpri	⊢ ( ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑇 ∈ ( 𝐹 ... ( ♯ ‘ 𝑆 ) ) ) )
28	27	simpld	⊢ ( ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
29	2 3 28	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
30		pfxlen	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
31	1 29 30	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
32	31	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
33	25 32	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
34	33	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) = ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
35	23 34	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
36		ccatval1	⊢ ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ 𝑋 ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) )
37	12 14 35 36	syl3anc	⊢ ( 𝜑 → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ 𝑋 ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) )
38	31	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) = ( 0 ..^ 𝐹 ) )
39	5 38	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) )
40		ccatval1	⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) )
41	10 4 39 40	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) )
42		pfxfv	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 0 ..^ 𝐹 ) ) → ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
43	1 29 5 42	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
44	41 43	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
45	8 37 44	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )