Step |
Hyp |
Ref |
Expression |
1 |
|
swrdccatin2.l |
|- L = ( # ` A ) |
2 |
|
pfxccatpfx2.m |
|- M = ( # ` B ) |
3 |
|
ccatcl |
|- ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V ) |
4 |
3
|
3adant3 |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A ++ B ) e. Word V ) |
5 |
|
lencl |
|- ( A e. Word V -> ( # ` A ) e. NN0 ) |
6 |
1 5
|
eqeltrid |
|- ( A e. Word V -> L e. NN0 ) |
7 |
|
elfzuz |
|- ( N e. ( ( L + 1 ) ... ( L + M ) ) -> N e. ( ZZ>= ` ( L + 1 ) ) ) |
8 |
|
peano2nn0 |
|- ( L e. NN0 -> ( L + 1 ) e. NN0 ) |
9 |
8
|
anim1i |
|- ( ( L e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) ) |
10 |
6 7 9
|
syl2an |
|- ( ( A e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) ) |
11 |
10
|
3adant2 |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) ) |
12 |
|
eluznn0 |
|- ( ( ( L + 1 ) e. NN0 /\ N e. ( ZZ>= ` ( L + 1 ) ) ) -> N e. NN0 ) |
13 |
11 12
|
syl |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> N e. NN0 ) |
14 |
|
pfxval |
|- ( ( ( A ++ B ) e. Word V /\ N e. NN0 ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) ) |
15 |
4 13 14
|
syl2anc |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( ( A ++ B ) substr <. 0 , N >. ) ) |
16 |
|
3simpa |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A e. Word V /\ B e. Word V ) ) |
17 |
6
|
3ad2ant1 |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> L e. NN0 ) |
18 |
|
0elfz |
|- ( L e. NN0 -> 0 e. ( 0 ... L ) ) |
19 |
17 18
|
syl |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> 0 e. ( 0 ... L ) ) |
20 |
5
|
nn0zd |
|- ( A e. Word V -> ( # ` A ) e. ZZ ) |
21 |
1 20
|
eqeltrid |
|- ( A e. Word V -> L e. ZZ ) |
22 |
21
|
adantr |
|- ( ( A e. Word V /\ B e. Word V ) -> L e. ZZ ) |
23 |
|
uzid |
|- ( L e. ZZ -> L e. ( ZZ>= ` L ) ) |
24 |
22 23
|
syl |
|- ( ( A e. Word V /\ B e. Word V ) -> L e. ( ZZ>= ` L ) ) |
25 |
|
peano2uz |
|- ( L e. ( ZZ>= ` L ) -> ( L + 1 ) e. ( ZZ>= ` L ) ) |
26 |
|
fzss1 |
|- ( ( L + 1 ) e. ( ZZ>= ` L ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + M ) ) ) |
27 |
24 25 26
|
3syl |
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + M ) ) ) |
28 |
2
|
eqcomi |
|- ( # ` B ) = M |
29 |
28
|
oveq2i |
|- ( L + ( # ` B ) ) = ( L + M ) |
30 |
29
|
oveq2i |
|- ( L ... ( L + ( # ` B ) ) ) = ( L ... ( L + M ) ) |
31 |
27 30
|
sseqtrrdi |
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( L + 1 ) ... ( L + M ) ) C_ ( L ... ( L + ( # ` B ) ) ) ) |
32 |
31
|
sseld |
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( ( L + 1 ) ... ( L + M ) ) -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) |
33 |
32
|
3impia |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> N e. ( L ... ( L + ( # ` B ) ) ) ) |
34 |
19 33
|
jca |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( 0 e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) |
35 |
1
|
pfxccatin12 |
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( 0 e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) |
36 |
16 34 35
|
sylc |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) substr <. 0 , N >. ) = ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) ) |
37 |
1
|
opeq2i |
|- <. 0 , L >. = <. 0 , ( # ` A ) >. |
38 |
37
|
oveq2i |
|- ( A substr <. 0 , L >. ) = ( A substr <. 0 , ( # ` A ) >. ) |
39 |
|
pfxval |
|- ( ( A e. Word V /\ ( # ` A ) e. NN0 ) -> ( A prefix ( # ` A ) ) = ( A substr <. 0 , ( # ` A ) >. ) ) |
40 |
5 39
|
mpdan |
|- ( A e. Word V -> ( A prefix ( # ` A ) ) = ( A substr <. 0 , ( # ` A ) >. ) ) |
41 |
|
pfxid |
|- ( A e. Word V -> ( A prefix ( # ` A ) ) = A ) |
42 |
40 41
|
eqtr3d |
|- ( A e. Word V -> ( A substr <. 0 , ( # ` A ) >. ) = A ) |
43 |
38 42
|
eqtrid |
|- ( A e. Word V -> ( A substr <. 0 , L >. ) = A ) |
44 |
43
|
3ad2ant1 |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( A substr <. 0 , L >. ) = A ) |
45 |
44
|
oveq1d |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A substr <. 0 , L >. ) ++ ( B prefix ( N - L ) ) ) = ( A ++ ( B prefix ( N - L ) ) ) ) |
46 |
15 36 45
|
3eqtrd |
|- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) ) |