Metamath Proof Explorer

Theorem splval2

Description: Value of a splice, assuming the input word S has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses splval2.a 
|- ( ph -> A e. Word X )
splval2.b 
|- ( ph -> B e. Word X )
splval2.c 
|- ( ph -> C e. Word X )
splval2.r 
|- ( ph -> R e. Word X )
splval2.s 
|- ( ph -> S = ( ( A ++ B ) ++ C ) )
splval2.f 
|- ( ph -> F = ( # ` A ) )
splval2.t 
|- ( ph -> T = ( F + ( # ` B ) ) )
Assertion splval2 
|- ( ph -> ( S splice <. F , T , R >. ) = ( ( A ++ R ) ++ C ) )

Proof

Step Hyp Ref Expression
1 splval2.a 
 |-  ( ph -> A e. Word X )
2 splval2.b 
 |-  ( ph -> B e. Word X )
3 splval2.c 
 |-  ( ph -> C e. Word X )
4 splval2.r 
 |-  ( ph -> R e. Word X )
5 splval2.s 
 |-  ( ph -> S = ( ( A ++ B ) ++ C ) )
6 splval2.f 
 |-  ( ph -> F = ( # ` A ) )
7 splval2.t 
 |-  ( ph -> T = ( F + ( # ` B ) ) )
8 ccatcl 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( A ++ B ) e. Word X )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A ++ B ) e. Word X )
10 ccatcl 
 |-  ( ( ( A ++ B ) e. Word X /\ C e. Word X ) -> ( ( A ++ B ) ++ C ) e. Word X )
11 9 3 10 syl2anc 
 |-  ( ph -> ( ( A ++ B ) ++ C ) e. Word X )
12 5 11 eqeltrd 
 |-  ( ph -> S e. Word X )
13 lencl 
 |-  ( A e. Word X -> ( # ` A ) e. NN0 )
14 1 13 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
15 6 14 eqeltrd 
 |-  ( ph -> F e. NN0 )
16 lencl 
 |-  ( B e. Word X -> ( # ` B ) e. NN0 )
17 2 16 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
18 15 17 nn0addcld 
 |-  ( ph -> ( F + ( # ` B ) ) e. NN0 )
19 7 18 eqeltrd 
 |-  ( ph -> T e. NN0 )
20 splval 
 |-  ( ( S e. Word X /\ ( F e. NN0 /\ T e. NN0 /\ R e. Word X ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
21 12 15 19 4 20 syl13anc 
 |-  ( ph -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
22 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
23 15 22 eleqtrdi 
 |-  ( ph -> F e. ( ZZ>= ` 0 ) )
24 15 nn0zd 
 |-  ( ph -> F e. ZZ )
25 24 uzidd 
 |-  ( ph -> F e. ( ZZ>= ` F ) )
26 uzaddcl 
 |-  ( ( F e. ( ZZ>= ` F ) /\ ( # ` B ) e. NN0 ) -> ( F + ( # ` B ) ) e. ( ZZ>= ` F ) )
27 25 17 26 syl2anc 
 |-  ( ph -> ( F + ( # ` B ) ) e. ( ZZ>= ` F ) )
28 7 27 eqeltrd 
 |-  ( ph -> T e. ( ZZ>= ` F ) )
29 elfzuzb 
 |-  ( F e. ( 0 ... T ) <-> ( F e. ( ZZ>= ` 0 ) /\ T e. ( ZZ>= ` F ) ) )
30 23 28 29 sylanbrc 
 |-  ( ph -> F e. ( 0 ... T ) )
31 19 22 eleqtrdi 
 |-  ( ph -> T e. ( ZZ>= ` 0 ) )
32 ccatlen 
 |-  ( ( ( A ++ B ) e. Word X /\ C e. Word X ) -> ( # ` ( ( A ++ B ) ++ C ) ) = ( ( # ` ( A ++ B ) ) + ( # ` C ) ) )
33 9 3 32 syl2anc 
 |-  ( ph -> ( # ` ( ( A ++ B ) ++ C ) ) = ( ( # ` ( A ++ B ) ) + ( # ` C ) ) )
34 5 fveq2d 
 |-  ( ph -> ( # ` S ) = ( # ` ( ( A ++ B ) ++ C ) ) )
35 6 oveq1d 
 |-  ( ph -> ( F + ( # ` B ) ) = ( ( # ` A ) + ( # ` B ) ) )
36 ccatlen 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
37 1 2 36 syl2anc 
 |-  ( ph -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
38 35 7 37 3eqtr4d 
 |-  ( ph -> T = ( # ` ( A ++ B ) ) )
39 38 oveq1d 
 |-  ( ph -> ( T + ( # ` C ) ) = ( ( # ` ( A ++ B ) ) + ( # ` C ) ) )
40 33 34 39 3eqtr4d 
 |-  ( ph -> ( # ` S ) = ( T + ( # ` C ) ) )
41 19 nn0zd 
 |-  ( ph -> T e. ZZ )
42 41 uzidd 
 |-  ( ph -> T e. ( ZZ>= ` T ) )
43 lencl 
 |-  ( C e. Word X -> ( # ` C ) e. NN0 )
44 3 43 syl 
 |-  ( ph -> ( # ` C ) e. NN0 )
45 uzaddcl 
 |-  ( ( T e. ( ZZ>= ` T ) /\ ( # ` C ) e. NN0 ) -> ( T + ( # ` C ) ) e. ( ZZ>= ` T ) )
46 42 44 45 syl2anc 
 |-  ( ph -> ( T + ( # ` C ) ) e. ( ZZ>= ` T ) )
47 40 46 eqeltrd 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` T ) )
48 elfzuzb 
 |-  ( T e. ( 0 ... ( # ` S ) ) <-> ( T e. ( ZZ>= ` 0 ) /\ ( # ` S ) e. ( ZZ>= ` T ) ) )
49 31 47 48 sylanbrc 
 |-  ( ph -> T e. ( 0 ... ( # ` S ) ) )
50 ccatpfx 
 |-  ( ( S e. Word X /\ F e. ( 0 ... T ) /\ T e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix F ) ++ ( S substr <. F , T >. ) ) = ( S prefix T ) )
51 12 30 49 50 syl3anc 
 |-  ( ph -> ( ( S prefix F ) ++ ( S substr <. F , T >. ) ) = ( S prefix T ) )
52 lencl 
 |-  ( S e. Word X -> ( # ` S ) e. NN0 )
53 12 52 syl 
 |-  ( ph -> ( # ` S ) e. NN0 )
54 53 22 eleqtrdi 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` 0 ) )
55 eluzfz2 
 |-  ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
56 54 55 syl 
 |-  ( ph -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
57 ccatpfx 
 |-  ( ( S e. Word X /\ T e. ( 0 ... ( # ` S ) ) /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix T ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( S prefix ( # ` S ) ) )
58 12 49 56 57 syl3anc 
 |-  ( ph -> ( ( S prefix T ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( S prefix ( # ` S ) ) )
59 pfxid 
 |-  ( S e. Word X -> ( S prefix ( # ` S ) ) = S )
60 12 59 syl 
 |-  ( ph -> ( S prefix ( # ` S ) ) = S )
61 58 60 5 3eqtrd 
 |-  ( ph -> ( ( S prefix T ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( ( A ++ B ) ++ C ) )
62 pfxcl 
 |-  ( S e. Word X -> ( S prefix T ) e. Word X )
63 12 62 syl 
 |-  ( ph -> ( S prefix T ) e. Word X )
64 swrdcl 
 |-  ( S e. Word X -> ( S substr <. T , ( # ` S ) >. ) e. Word X )
65 12 64 syl 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) e. Word X )
66 pfxlen 
 |-  ( ( S e. Word X /\ T e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix T ) ) = T )
67 12 49 66 syl2anc 
 |-  ( ph -> ( # ` ( S prefix T ) ) = T )
68 67 38 eqtrd 
 |-  ( ph -> ( # ` ( S prefix T ) ) = ( # ` ( A ++ B ) ) )
69 ccatopth 
 |-  ( ( ( ( S prefix T ) e. Word X /\ ( S substr <. T , ( # ` S ) >. ) e. Word X ) /\ ( ( A ++ B ) e. Word X /\ C e. Word X ) /\ ( # ` ( S prefix T ) ) = ( # ` ( A ++ B ) ) ) -> ( ( ( S prefix T ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( ( A ++ B ) ++ C ) <-> ( ( S prefix T ) = ( A ++ B ) /\ ( S substr <. T , ( # ` S ) >. ) = C ) ) )
70 63 65 9 3 68 69 syl221anc 
 |-  ( ph -> ( ( ( S prefix T ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( ( A ++ B ) ++ C ) <-> ( ( S prefix T ) = ( A ++ B ) /\ ( S substr <. T , ( # ` S ) >. ) = C ) ) )
71 61 70 mpbid 
 |-  ( ph -> ( ( S prefix T ) = ( A ++ B ) /\ ( S substr <. T , ( # ` S ) >. ) = C ) )
72 71 simpld 
 |-  ( ph -> ( S prefix T ) = ( A ++ B ) )
73 51 72 eqtrd 
 |-  ( ph -> ( ( S prefix F ) ++ ( S substr <. F , T >. ) ) = ( A ++ B ) )
74 pfxcl 
 |-  ( S e. Word X -> ( S prefix F ) e. Word X )
75 12 74 syl 
 |-  ( ph -> ( S prefix F ) e. Word X )
76 swrdcl 
 |-  ( S e. Word X -> ( S substr <. F , T >. ) e. Word X )
77 12 76 syl 
 |-  ( ph -> ( S substr <. F , T >. ) e. Word X )
78 uztrn 
 |-  ( ( ( # ` S ) e. ( ZZ>= ` T ) /\ T e. ( ZZ>= ` F ) ) -> ( # ` S ) e. ( ZZ>= ` F ) )
79 47 28 78 syl2anc 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` F ) )
80 elfzuzb 
 |-  ( F e. ( 0 ... ( # ` S ) ) <-> ( F e. ( ZZ>= ` 0 ) /\ ( # ` S ) e. ( ZZ>= ` F ) ) )
81 23 79 80 sylanbrc 
 |-  ( ph -> F e. ( 0 ... ( # ` S ) ) )
82 pfxlen 
 |-  ( ( S e. Word X /\ F e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix F ) ) = F )
83 12 81 82 syl2anc 
 |-  ( ph -> ( # ` ( S prefix F ) ) = F )
84 83 6 eqtrd 
 |-  ( ph -> ( # ` ( S prefix F ) ) = ( # ` A ) )
85 ccatopth 
 |-  ( ( ( ( S prefix F ) e. Word X /\ ( S substr <. F , T >. ) e. Word X ) /\ ( A e. Word X /\ B e. Word X ) /\ ( # ` ( S prefix F ) ) = ( # ` A ) ) -> ( ( ( S prefix F ) ++ ( S substr <. F , T >. ) ) = ( A ++ B ) <-> ( ( S prefix F ) = A /\ ( S substr <. F , T >. ) = B ) ) )
86 75 77 1 2 84 85 syl221anc 
 |-  ( ph -> ( ( ( S prefix F ) ++ ( S substr <. F , T >. ) ) = ( A ++ B ) <-> ( ( S prefix F ) = A /\ ( S substr <. F , T >. ) = B ) ) )
87 73 86 mpbid 
 |-  ( ph -> ( ( S prefix F ) = A /\ ( S substr <. F , T >. ) = B ) )
88 87 simpld 
 |-  ( ph -> ( S prefix F ) = A )
89 88 oveq1d 
 |-  ( ph -> ( ( S prefix F ) ++ R ) = ( A ++ R ) )
90 71 simprd 
 |-  ( ph -> ( S substr <. T , ( # ` S ) >. ) = C )
91 89 90 oveq12d 
 |-  ( ph -> ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) = ( ( A ++ R ) ++ C ) )
92 21 91 eqtrd 
 |-  ( ph -> ( S splice <. F , T , R >. ) = ( ( A ++ R ) ++ C ) )