Metamath Proof Explorer

Theorem spllen

Description: The length of a splice. (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 )
Assertion spllen 
|- ( ph -> ( # ` ( S splice <. F , T , R >. ) ) = ( ( # ` S ) + ( ( # ` R ) - ( T - F ) ) ) )

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 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 ) >. ) ) )
6 1 2 3 4 5 syl13anc 
 |-  ( ph -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
7 6 fveq2d 
 |-  ( ph -> ( # ` ( S splice <. F , T , R >. ) ) = ( # ` ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) )
8 pfxcl 
 |-  ( S e. Word A -> ( S prefix F ) e. Word A )
9 1 8 syl 
 |-  ( ph -> ( S prefix F ) e. Word A )
10 ccatcl 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( ( S prefix F ) ++ R ) e. Word A )
11 9 4 10 syl2anc 
 |-  ( ph -> ( ( S prefix F ) ++ R ) e. Word A )
12 swrdcl 
 |-  ( S e. Word A -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
13 1 12 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word A )
14 ccatlen 
 |-  ( ( ( ( S prefix F ) ++ R ) e. Word A /\ ( S substr <. T , ( # ` S ) >. ) e. Word A ) -> ( # ` ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( # ` ( ( S prefix F ) ++ R ) ) + ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) )
15 11 13 14 syl2anc 
 |-  ( ph -> ( # ` ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( # ` ( ( S prefix F ) ++ R ) ) + ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) )
16 lencl 
 |-  ( R e. Word A -> ( # ` R ) e. NN0 )
17 16 nn0cnd 
 |-  ( R e. Word A -> ( # ` R ) e. CC )
18 4 17 syl 
 |-  ( ph -> ( # ` R ) e. CC )
19 elfzelz 
 |-  ( F e. ( 0 ... T ) -> F e. ZZ )
20 19 zcnd 
 |-  ( F e. ( 0 ... T ) -> F e. CC )
21 2 20 syl 
 |-  ( ph -> F e. CC )
22 18 21 addcld 
 |-  ( ph -> ( ( # ` R ) + F ) e. CC )
23 elfzel2 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ZZ )
24 23 zcnd 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. CC )
25 3 24 syl 
 |-  ( ph -> ( # ` S ) e. CC )
26 elfzelz 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> T e. ZZ )
27 26 zcnd 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> T e. CC )
28 3 27 syl 
 |-  ( ph -> T e. CC )
29 22 25 28 addsub12d 
 |-  ( ph -> ( ( ( # ` R ) + F ) + ( ( # ` S ) - T ) ) = ( ( # ` S ) + ( ( ( # ` R ) + F ) - T ) ) )
30 ccatlen 
 |-  ( ( ( S prefix F ) e. Word A /\ R e. Word A ) -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
31 9 4 30 syl2anc 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` ( S prefix F ) ) + ( # ` R ) ) )
32 elfzuz 
 |-  ( F e. ( 0 ... T ) -> F e. ( ZZ>= ` 0 ) )
33 2 32 syl 
 |-  ( ph -> F e. ( ZZ>= ` 0 ) )
34 elfzuz3 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` T ) )
35 3 34 syl 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` T ) )
36 elfzuz3 
 |-  ( F e. ( 0 ... T ) -> T e. ( ZZ>= ` F ) )
37 2 36 syl 
 |-  ( ph -> T e. ( ZZ>= ` F ) )
38 uztrn 
 |-  ( ( ( # ` S ) e. ( ZZ>= ` T ) /\ T e. ( ZZ>= ` F ) ) -> ( # ` S ) e. ( ZZ>= ` F ) )
39 35 37 38 syl2anc 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` F ) )
40 elfzuzb 
 |-  ( F e. ( 0 ... ( # ` S ) ) <-> ( F e. ( ZZ>= ` 0 ) /\ ( # ` S ) e. ( ZZ>= ` F ) ) )
41 33 39 40 sylanbrc 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
42 pfxlen 
 |-  ( ( S e. Word A /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
43 1 41 42 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
44 43 oveq1d 
 |-  ( ph -> ( ( # ` ( S prefix F ) ) + ( # ` R ) ) = ( F + ( # ` R ) ) )
45 21 18 addcomd 
 |-  ( ph -> ( F + ( # ` R ) ) = ( ( # ` R ) + F ) )
46 31 44 45 3eqtrd 
 |-  ( ph -> ( # ` ( ( S prefix F ) ++ R ) ) = ( ( # ` R ) + F ) )
47 elfzuz2 
 |-  ( T e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` 0 ) )
48 eluzfz2 
 |-  ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
49 3 47 48 3syl 
 |-  ( ph -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
50 swrdlen 
 |-  ( ( S e. Word A /\ T e. ( 0 ... ( # ` S ) ) /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. T , ( # ` S ) >. ) ) = ( ( # ` S ) - T ) )
51 1 3 49 50 syl3anc 
 |-  ( ph -> ( # ` ( S substr <. T , ( # ` S ) >. ) ) = ( ( # ` S ) - T ) )
52 46 51 oveq12d 
 |-  ( ph -> ( ( # ` ( ( S prefix F ) ++ R ) ) + ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( ( # ` R ) + F ) + ( ( # ` S ) - T ) ) )
53 18 28 21 subsub3d 
 |-  ( ph -> ( ( # ` R ) - ( T - F ) ) = ( ( ( # ` R ) + F ) - T ) )
54 53 oveq2d 
 |-  ( ph -> ( ( # ` S ) + ( ( # ` R ) - ( T - F ) ) ) = ( ( # ` S ) + ( ( ( # ` R ) + F ) - T ) ) )
55 29 52 54 3eqtr4d 
 |-  ( ph -> ( ( # ` ( ( S prefix F ) ++ R ) ) + ( # ` ( S substr <. T , ( # ` S ) >. ) ) ) = ( ( # ` S ) + ( ( # ` R ) - ( T - F ) ) ) )
56 7 15 55 3eqtrd 
 |-  ( ph -> ( # ` ( S splice <. F , T , R >. ) ) = ( ( # ` S ) + ( ( # ` R ) - ( T - F ) ) ) )