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 elfzelz 
 |-  ( F e. ( 0 ... T ) -> F e. ZZ )
16 2 15 syl 
 |-  ( ph -> F e. ZZ )
17 16 uzidd 
 |-  ( ph -> F e. ( ZZ>= ` F ) )
18 lencl 
 |-  ( R e. Word A -> ( # ` R ) e. NN0 )
19 4 18 syl 
 |-  ( ph -> ( # ` R ) e. NN0 )
20 uzaddcl 
 |-  ( ( F e. ( ZZ>= ` F ) /\ ( # ` R ) e. NN0 ) -> ( F + ( # ` R ) ) e. ( ZZ>= ` F ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ( F + ( # ` R ) ) e. ( ZZ>= ` F ) )
22 fzoss2 
 |-  ( ( F + ( # ` R ) ) e. ( ZZ>= ` F ) -> ( 0 ..^ F ) C_ ( 0 ..^ ( F + ( # ` R ) ) ) )
23 21 22 syl 
 |-  ( ph -> ( 0 ..^ F ) C_ ( 0 ..^ ( F + ( # ` R ) ) ) )
24 23 5 sseldd 
 |-  ( ph -> X e. ( 0 ..^ ( F + ( # ` R ) ) ) )
25 ccatlen 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
26 10 4 25 syl2anc 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
27 fzass4 
 |-  ( ( F e. ( 0 ... ( # ` S ) ) /\ T e. ( F ... ( # ` S ) ) ) <-> ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) )
28 27 biimpri 
 |-  ( ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) -> ( F e. ( 0 ... ( # ` S ) ) /\ T e. ( F ... ( # ` S ) ) ) )
29 28 simpld 
 |-  ( ( F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) -> F e. ( 0 ... ( # ` S ) ) )
30 2 3 29 syl2anc 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
31 pfxlen 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
32 1 30 31 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
33 32 oveq1d 
 |-  ( ph -> ( ( # ` ( S prefix F ) ) + ( # ` R ) ) = ( F + ( # ` R ) ) )
34 26 33 eqtrd 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( F + ( # ` R ) ) )
35 34 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) = ( 0 ..^ ( F + ( # ` R ) ) ) )
36 24 35 eleqtrrd 
 |-  ( ph -> X e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) )
37 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 ) )
38 12 14 36 37 syl3anc 
 |-  ( ph -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` X ) = ( ( ( S prefix F ) ++ R ) ` X ) )
39 32 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( S prefix F ) ) ) = ( 0 ..^ F ) )
40 5 39 eleqtrrd 
 |-  ( ph -> X e. ( 0 ..^ ( # ` ( S prefix F ) ) ) )
41 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 ) )
42 10 4 40 41 syl3anc 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ` X ) = ( ( S prefix F ) ` X ) )
43 pfxfv 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) /\ X e. ( 0 ..^ F ) ) -> ( ( S prefix F ) ` X ) = ( S ` X ) )
44 1 30 5 43 syl3anc 
 |-  ( ph -> ( ( S prefix F ) ` X ) = ( S ` X ) )
45 42 44 eqtrd 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ` X ) = ( S ` X ) )
46 8 38 45 3eqtrd 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` X ) = ( S ` X ) )