Metamath Proof Explorer

Theorem splfv3

Description: Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 splfv3.s ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
2 splfv3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
3 splfv3.t ⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
4 splfv3.r ⊢ ( 𝜑 → 𝑅 ∈ Word 𝐴 )
5 splfv3.x ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) − 𝑇 ) ) )
6 splfv3.k ⊢ ( 𝜑 → 𝐾 = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
7 splval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑅 ∈ Word 𝐴 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
8 1 2 3 4 7 syl13anc ⊢ ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
9 elfzuz3 ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝑇 ) )
10 fzss2 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝑇 ) → ( 0 ... 𝑇 ) ⊆ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
11 3 9 10 3syl ⊢ ( 𝜑 → ( 0 ... 𝑇 ) ⊆ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
12 11 2 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
13 pfxlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
14 1 12 13 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
15 14 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
16 pfxcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
17 1 16 syl ⊢ ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
18 ccatlen ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
19 17 4 18 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
20 15 19 6 3eqtr4rd ⊢ ( 𝜑 → 𝐾 = ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) )
21 20 oveq2d ⊢ ( 𝜑 → ( 𝑋 + 𝐾 ) = ( 𝑋 + ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
22 8 21 fveq12d ⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ ( 𝑋 + 𝐾 ) ) = ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) )
23 ccatcl ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
24 17 4 23 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
25 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
26 1 25 syl ⊢ ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
27 lencl ⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
28 nn0fz0 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
29 27 28 sylib ⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
30 1 29 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
31 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) − 𝑇 ) )
32 1 3 30 31 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) − 𝑇 ) )
33 32 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) − 𝑇 ) ) )
34 5 33 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
35 ccatval3 ⊢ ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) ) → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) = ( ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ‘ 𝑋 ) )
36 24 26 34 35 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) = ( ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ‘ 𝑋 ) )
37 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑋 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) − 𝑇 ) ) ) → ( ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ ( 𝑋 + 𝑇 ) ) )
38 1 3 30 5 37 syl31anc ⊢ ( 𝜑 → ( ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ ( 𝑋 + 𝑇 ) ) )
39 22 36 38 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ ( 𝑋 + 𝐾 ) ) = ( 𝑆 ‘ ( 𝑋 + 𝑇 ) ) )