Step |
Hyp |
Ref |
Expression |
1 |
|
lencl |
|- ( W e. Word V -> ( # ` W ) e. NN0 ) |
2 |
|
nn0fz0 |
|- ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
3 |
1 2
|
sylib |
|- ( W e. Word V -> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
4 |
3
|
adantr |
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
5 |
|
ccatpfx |
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) ) |
6 |
4 5
|
mpd3an3 |
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) ) |
7 |
|
pfxid |
|- ( W e. Word V -> ( W prefix ( # ` W ) ) = W ) |
8 |
7
|
adantr |
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( W prefix ( # ` W ) ) = W ) |
9 |
6 8
|
eqtrd |
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) = W ) |