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

Proof

Step Hyp Ref Expression
1 splfv3.s 
 |-  ( ph -> S e. Word A )
2 splfv3.f 
 |-  ( ph -> F e. ( 0 ... T ) )
3 splfv3.t 
 |-  ( ph -> T e. ( 0 ... ( # ` S ) ) )
4 splfv3.r 
 |-  ( ph -> R e. Word A )
5 splfv3.x 
 |-  ( ph -> X e. ( 0 ..^ ( ( # ` S ) - T ) ) )
6 splfv3.k 
 |-  ( ph -> K = ( F + ( # ` R ) ) )
7 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 ) >. ) ) )
8 1 2 3 4 7 syl13anc 
 |-  ( ph -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
9 elfzuz3 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` T ) )
10 fzss2 
 |-  ( ( # ` S ) e. ( ZZ>= ` T ) -> ( 0 ... T ) C_ ( 0 ... ( # ` S ) ) )
11 3 9 10 3syl 
 |-  ( ph -> ( 0 ... T ) C_ ( 0 ... ( # ` S ) ) )
12 11 2 sseldd 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
13 pfxlen 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
14 1 12 13 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
15 14 oveq1d 
 |-  ( ph -> ( ( # ` ( S prefix F ) ) + ( # ` R ) ) = ( F + ( # ` R ) ) )
16 pfxcl 
 |-  ( S e. Word A -> ( S prefix F ) e. Word A )
17 1 16 syl 
 |-  ( ph -> ( S prefix F ) e. Word A )
18 ccatlen 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
19 17 4 18 syl2anc 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
20 15 19 6 3eqtr4rd 
 |-  ( ph -> K = ( # ` ( ( S prefix F ) ++ R ) ) )
21 20 oveq2d 
 |-  ( ph -> ( X + K ) = ( X + ( # ` ( ( S prefix F ) ++ R ) ) ) )
22 8 21 fveq12d 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` ( X + K ) ) = ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( ( S prefix F ) ++ R ) ) ) ) )
23 ccatcl 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( ( S prefix F ) ++ R ) e. Word A )
24 17 4 23 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ R ) e. Word A )
25 swrdcl 
 |-  ( S e. Word A -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
26 1 25 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
27 lencl 
 |-  ( S e. Word A -> ( # ` S ) e. NN0 )
28 nn0fz0 
 |-  ( ( # ` S ) e. NN0 <-> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
29 27 28 sylib 
 |-  ( S e. Word A -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
30 1 29 syl 
 |-  ( ph -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
31 swrdlen 
 |-  ( ( S e. Word A /\ T e. ( 0 ... ( # ` S ) ) /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. T , ( # ` S ) >. ) ) = ( ( # ` S ) - T ) )
32 1 3 30 31 syl3anc 
 |-  ( ph -> ( # ` ( S substr <. T , ( # ` S ) >. ) ) = ( ( # ` S ) - T ) )
33 32 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) = ( 0 ..^ ( ( # ` S ) - T ) ) )
34 5 33 eleqtrrd 
 |-  ( ph -> X e. ( 0 ..^ ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) )
35 ccatval3 
 |-  ( ( ( ( S prefix F ) ++ R ) e. Word A /\ ( S substr <. T , ( # ` S ) >. ) e. Word A /\ X e. ( 0 ..^ ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) ) -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( ( S prefix F ) ++ R ) ) ) ) = ( ( S substr <. T , ( # ` S ) >. ) ` X ) )
36 24 26 34 35 syl3anc 
 |-  ( ph -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( ( S prefix F ) ++ R ) ) ) ) = ( ( S substr <. T , ( # ` S ) >. ) ` X ) )
37 swrdfv 
 |-  ( ( ( S e. Word A /\ T e. ( 0 ... ( # ` S ) ) /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) /\ X e. ( 0 ..^ ( ( # ` S ) - T ) ) ) -> ( ( S substr <. T , ( # ` S ) >. ) ` X ) = ( S ` ( X + T ) ) )
38 1 3 30 5 37 syl31anc 
 |-  ( ph -> ( ( S substr <. T , ( # ` S ) >. ) ` X ) = ( S ` ( X + T ) ) )
39 22 36 38 3eqtrd 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` ( X + K ) ) = ( S ` ( X + T ) ) )