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 
|- ( ph -> S e. Word A )
spllen.f 
|- ( ph -> F e. ( 0 ... T ) )
spllen.t 
|- ( ph -> T e. ( 0 ... ( # ` S ) ) )
spllen.r 
|- ( ph -> R e. Word A )
splfv1.x 
|- ( ph -> X e. ( 0 ..^ F ) )
Assertion splfv1 
|- ( ph -> ( ( S splice <. F , T , R >. ) ` X ) = ( S ` X ) )

Proof

Step Hyp Ref Expression
1 spllen.s 
 |-  ( ph -> S e. Word A )
2 spllen.f 
 |-  ( ph -> F e. ( 0 ... T ) )
3 spllen.t 
 |-  ( ph -> T e. ( 0 ... ( # ` S ) ) )
4 spllen.r 
 |-  ( ph -> R e. Word A )
5 splfv1.x 
 |-  ( ph -> X e. ( 0 ..^ F ) )
6 splval 
 |-  ( ( S e. Word A /\ ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) /\ R e. Word A ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
7 1 2 3 4 6 syl13anc 
 |-  ( ph -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
8 7 fveq1d 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` X ) = ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` X ) )
9 pfxcl 
 |-  ( S e. Word A -> ( S prefix F ) e. Word A )
10 1 9 syl 
 |-  ( ph -> ( S prefix F ) e. Word A )
11 ccatcl 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( ( S prefix F ) ++ R ) e. Word A )
12 10 4 11 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ R ) e. Word A )
13 swrdcl 
 |-  ( S e. Word A -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
14 1 13 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
15 2 elfzelzd 
 |-  ( ph -> F e. ZZ )
16 15 uzidd 
 |-  ( ph -> F e. ( ZZ>= ` F ) )
17 lencl 
 |-  ( R e. Word A -> ( # ` R ) e. NN0 )
18 4 17 syl 
 |-  ( ph -> ( # ` R ) e. NN0 )
19 uzaddcl 
 |-  ( ( F e. ( ZZ>= ` F ) /\ ( # ` R ) e. NN0 ) -> ( F + ( # ` R ) ) e. ( ZZ>= ` F ) )
20 16 18 19 syl2anc 
 |-  ( ph -> ( F + ( # ` R ) ) e. ( ZZ>= ` F ) )
21 fzoss2 
 |-  ( ( F + ( # ` R ) ) e. ( ZZ>= ` F ) -> ( 0 ..^ F ) C_ ( 0 ..^ ( F + ( # ` R ) ) ) )
22 20 21 syl 
 |-  ( ph -> ( 0 ..^ F ) C_ ( 0 ..^ ( F + ( # ` R ) ) ) )
23 22 5 sseldd 
 |-  ( ph -> X e. ( 0 ..^ ( F + ( # ` R ) ) ) )
24 ccatlen 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
25 10 4 24 syl2anc 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
26 fzass4 
 |-  ( ( F e. ( 0 ... ( # ` S ) ) /\ T e. ( F ... ( # ` S ) ) ) <-> ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) )
27 26 biimpri 
 |-  ( ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) -> ( F e. ( 0 ... ( # ` S ) ) /\ T e. ( F ... ( # ` S ) ) ) )
28 27 simpld 
 |-  ( ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) -> F e. ( 0 ... ( # ` S ) ) )
29 2 3 28 syl2anc 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
30 pfxlen 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
31 1 29 30 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
32 31 oveq1d 
 |-  ( ph -> ( ( # ` ( S prefix F ) ) + ( # ` R ) ) = ( F + ( # ` R ) ) )
33 25 32 eqtrd 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( F + ( # ` R ) ) )
34 33 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) = ( 0 ..^ ( F + ( # ` R ) ) ) )
35 23 34 eleqtrrd 
 |-  ( ph -> X e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) )
36 ccatval1 
 |-  ( ( ( ( S prefix F ) ++ R ) e. Word A /\ ( S substr <. T , ( # ` S ) >. ) e. Word A /\ X e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) ) -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` X ) = ( ( ( S prefix F ) ++ R ) ` X ) )
37 12 14 35 36 syl3anc 
 |-  ( ph -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` X ) = ( ( ( S prefix F ) ++ R ) ` X ) )
38 31 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( S prefix F ) ) ) = ( 0 ..^ F ) )
39 5 38 eleqtrrd 
 |-  ( ph -> X e. ( 0 ..^ ( # ` ( S prefix F ) ) ) )
40 ccatval1 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A /\ X e. ( 0 ..^ ( # ` ( S prefix F ) ) ) ) -> ( ( ( S prefix F ) ++ R ) ` X ) = ( ( S prefix F ) ` X ) )
41 10 4 39 40 syl3anc 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ` X ) = ( ( S prefix F ) ` X ) )
42 pfxfv 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) /\ X e. ( 0 ..^ F ) ) -> ( ( S prefix F ) ` X ) = ( S ` X ) )
43 1 29 5 42 syl3anc 
 |-  ( ph -> ( ( S prefix F ) ` X ) = ( S ` X ) )
44 41 43 eqtrd 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ` X ) = ( S ` X ) )
45 8 37 44 3eqtrd 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` X ) = ( S ` X ) )