Description: A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | swrdccatin2.l | |
|
pfxccatpfx2.m | |
||
Assertion | pfxccatpfx2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swrdccatin2.l | |
|
2 | pfxccatpfx2.m | |
|
3 | ccatcl | |
|
4 | 3 | 3adant3 | |
5 | lencl | |
|
6 | 1 5 | eqeltrid | |
7 | elfzuz | |
|
8 | peano2nn0 | |
|
9 | 8 | anim1i | |
10 | 6 7 9 | syl2an | |
11 | 10 | 3adant2 | |
12 | eluznn0 | |
|
13 | 11 12 | syl | |
14 | pfxval | |
|
15 | 4 13 14 | syl2anc | |
16 | 3simpa | |
|
17 | 6 | 3ad2ant1 | |
18 | 0elfz | |
|
19 | 17 18 | syl | |
20 | 5 | nn0zd | |
21 | 1 20 | eqeltrid | |
22 | 21 | adantr | |
23 | uzid | |
|
24 | 22 23 | syl | |
25 | peano2uz | |
|
26 | fzss1 | |
|
27 | 24 25 26 | 3syl | |
28 | 2 | eqcomi | |
29 | 28 | oveq2i | |
30 | 29 | oveq2i | |
31 | 27 30 | sseqtrrdi | |
32 | 31 | sseld | |
33 | 32 | 3impia | |
34 | 19 33 | jca | |
35 | 1 | pfxccatin12 | |
36 | 16 34 35 | sylc | |
37 | 1 | opeq2i | |
38 | 37 | oveq2i | |
39 | pfxval | |
|
40 | 5 39 | mpdan | |
41 | pfxid | |
|
42 | 40 41 | eqtr3d | |
43 | 38 42 | eqtrid | |
44 | 43 | 3ad2ant1 | |
45 | 44 | oveq1d | |
46 | 15 36 45 | 3eqtrd | |