Metamath Proof Explorer

Theorem splfv2a

Description: Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (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 )
splfv2a.x 
|- ( ph -> X e. ( 0 ..^ ( # ` R ) ) )
Assertion splfv2a 
|- ( ph -> ( ( S splice <. F , T , R >. ) ` ( F + X ) ) = ( R ` 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 splfv2a.x 
 |-  ( ph -> X e. ( 0 ..^ ( # ` R ) ) )
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 elfznn0 
 |-  ( F e. ( 0 ... T ) -> F e. NN0 )
9 2 8 syl 
 |-  ( ph -> F e. NN0 )
10 9 nn0cnd 
 |-  ( ph -> F e. CC )
11 elfzonn0 
 |-  ( X e. ( 0 ..^ ( # ` R ) ) -> X e. NN0 )
12 5 11 syl 
 |-  ( ph -> X e. NN0 )
13 12 nn0cnd 
 |-  ( ph -> X e. CC )
14 10 13 addcomd 
 |-  ( ph -> ( F + X ) = ( X + F ) )
15 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
16 9 15 eleqtrdi 
 |-  ( ph -> F e. ( ZZ>= ` 0 ) )
17 elfzuz3 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` T ) )
18 3 17 syl 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` T ) )
19 elfzuz3 
 |-  ( F e. ( 0 ... T ) -> T e. ( ZZ>= ` F ) )
20 2 19 syl 
 |-  ( ph -> T e. ( ZZ>= ` F ) )
21 uztrn 
 |-  ( ( ( # ` S ) e. ( ZZ>= ` T ) /\ T e. ( ZZ>= ` F ) ) -> ( # ` S ) e. ( ZZ>= ` F ) )
22 18 20 21 syl2anc 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` F ) )
23 elfzuzb 
 |-  ( F e. ( 0 ... ( # ` S ) ) <-> ( F e. ( ZZ>= ` 0 ) /\ ( # ` S ) e. ( ZZ>= ` F ) ) )
24 16 22 23 sylanbrc 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
25 pfxlen 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
26 1 24 25 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
27 26 oveq2d 
 |-  ( ph -> ( X + ( # ` ( S prefix F ) ) ) = ( X + F ) )
28 14 27 eqtr4d 
 |-  ( ph -> ( F + X ) = ( X + ( # ` ( S prefix F ) ) ) )
29 7 28 fveq12d 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` ( F + X ) ) = ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( S prefix F ) ) ) ) )
30 pfxcl 
 |-  ( S e. Word A -> ( S prefix F ) e. Word A )
31 1 30 syl 
 |-  ( ph -> ( S prefix F ) e. Word A )
32 ccatcl 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( ( S prefix F ) ++ R ) e. Word A )
33 31 4 32 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ R ) e. Word A )
34 swrdcl 
 |-  ( S e. Word A -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
35 1 34 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
36 0nn0 
 |-  0 e. NN0
37 nn0addcl 
 |-  ( ( 0 e. NN0 /\ F e. NN0 ) -> ( 0 + F ) e. NN0 )
38 36 9 37 sylancr 
 |-  ( ph -> ( 0 + F ) e. NN0 )
39 fzoss1 
 |-  ( ( 0 + F ) e. ( ZZ>= ` 0 ) -> ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) C_ ( 0 ..^ ( ( # ` R ) + F ) ) )
40 39 15 eleq2s 
 |-  ( ( 0 + F ) e. NN0 -> ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) C_ ( 0 ..^ ( ( # ` R ) + F ) ) )
41 38 40 syl 
 |-  ( ph -> ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) C_ ( 0 ..^ ( ( # ` R ) + F ) ) )
42 ccatlen 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
43 31 4 42 syl2anc 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
44 26 oveq1d 
 |-  ( ph -> ( ( # ` ( S prefix F ) ) + ( # ` R ) ) = ( F + ( # ` R ) ) )
45 lencl 
 |-  ( R e. Word A -> ( # ` R ) e. NN0 )
46 4 45 syl 
 |-  ( ph -> ( # ` R ) e. NN0 )
47 46 nn0cnd 
 |-  ( ph -> ( # ` R ) e. CC )
48 10 47 addcomd 
 |-  ( ph -> ( F + ( # ` R ) ) = ( ( # ` R ) + F ) )
49 43 44 48 3eqtrd 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` R ) + F ) )
50 49 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) = ( 0 ..^ ( ( # ` R ) + F ) ) )
51 41 50 sseqtrrd 
 |-  ( ph -> ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) C_ ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) )
52 9 nn0zd 
 |-  ( ph -> F e. ZZ )
53 fzoaddel 
 |-  ( ( X e. ( 0 ..^ ( # ` R ) ) /\ F e. ZZ ) -> ( X + F ) e. ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) )
54 5 52 53 syl2anc 
 |-  ( ph -> ( X + F ) e. ( ( 0 + F ) ..^ ( ( # ` R ) + F ) ) )
55 51 54 sseldd 
 |-  ( ph -> ( X + F ) e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) )
56 27 55 eqeltrd 
 |-  ( ph -> ( X + ( # ` ( S prefix F ) ) ) e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) )
57 ccatval1 
 |-  ( ( ( ( S prefix F ) ++ R ) e. Word A /\ ( S substr <. T , ( # ` S ) >. ) e. Word A /\ ( X + ( # ` ( S prefix F ) ) ) e. ( 0 ..^ ( # ` ( ( S prefix F ) ++ R ) ) ) ) -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( S prefix F ) ) ) ) = ( ( ( S prefix F ) ++ R ) ` ( X + ( # ` ( S prefix F ) ) ) ) )
58 33 35 56 57 syl3anc 
 |-  ( ph -> ( ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ` ( X + ( # ` ( S prefix F ) ) ) ) = ( ( ( S prefix F ) ++ R ) ` ( X + ( # ` ( S prefix F ) ) ) ) )
59 ccatval3 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A /\ X e. ( 0 ..^ ( # ` R ) ) ) -> ( ( ( S prefix F ) ++ R ) ` ( X + ( # ` ( S prefix F ) ) ) ) = ( R ` X ) )
60 31 4 5 59 syl3anc 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ` ( X + ( # ` ( S prefix F ) ) ) ) = ( R ` X ) )
61 29 58 60 3eqtrd 
 |-  ( ph -> ( ( S splice <. F , T , R >. ) ` ( F + X ) ) = ( R ` X ) )