This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ 𝑋 ) = ( 𝑆 ‘ 𝑋 ) )