Metamath Proof Explorer

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 elfzelz ⊢ ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝐹 ∈ ℤ )
16 2 15 syl ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
17 16 uzidd ⊢ ( 𝜑 → 𝐹 ∈ ( ℤ≥ ‘ 𝐹 ) )
18 lencl ⊢ ( 𝑅 ∈ Word 𝐴 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
19 4 18 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
20 uzaddcl ⊢ ( ( 𝐹 ∈ ( ℤ≥ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝑅 ) ∈ ℕ0 ) → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) )
22 fzoss2 ⊢ ( ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ∈ ( ℤ≥ ‘ 𝐹 ) → ( 0 ..^ 𝐹 ) ⊆ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
23 21 22 syl ⊢ ( 𝜑 → ( 0 ..^ 𝐹 ) ⊆ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
24 23 5 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
25 ccatlen ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
26 10 4 25 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
27 fzass4 ⊢ ( ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑇 ∈ ( 𝐹 ... ( ♯ ‘ 𝑆 ) ) ) ↔ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
28 27 biimpri ⊢ ( ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑇 ∈ ( 𝐹 ... ( ♯ ‘ 𝑆 ) ) ) )
29 28 simpld ⊢ ( ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
30 2 3 29 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
31 pfxlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
32 1 30 31 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
33 32 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
34 26 33 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
35 34 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) = ( 0 ..^ ( 𝐹 + ( ♯ ‘ 𝑅 ) ) ) )
36 24 35 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
37 ccatval1 ⊢ ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ 𝑋 ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) )
38 12 14 36 37 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ 𝑋 ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) )
39 32 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) = ( 0 ..^ 𝐹 ) )
40 5 39 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) )
41 ccatval1 ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) )
42 10 4 40 41 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) )
43 pfxfv ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑋 ∈ ( 0 ..^ 𝐹 ) ) → ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
44 1 30 5 43 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
45 42 44 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )
46 8 38 45 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )