Metamath Proof Explorer


Theorem pfxccatpfx2

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 L=A
pfxccatpfx2.m M=B
Assertion pfxccatpfx2 AWordVBWordVNL+1L+MA++BprefixN=A++BprefixNL

Proof

Step Hyp Ref Expression
1 swrdccatin2.l L=A
2 pfxccatpfx2.m M=B
3 ccatcl AWordVBWordVA++BWordV
4 3 3adant3 AWordVBWordVNL+1L+MA++BWordV
5 lencl AWordVA0
6 1 5 eqeltrid AWordVL0
7 elfzuz NL+1L+MNL+1
8 peano2nn0 L0L+10
9 8 anim1i L0NL+1L+10NL+1
10 6 7 9 syl2an AWordVNL+1L+ML+10NL+1
11 10 3adant2 AWordVBWordVNL+1L+ML+10NL+1
12 eluznn0 L+10NL+1N0
13 11 12 syl AWordVBWordVNL+1L+MN0
14 pfxval A++BWordVN0A++BprefixN=A++Bsubstr0N
15 4 13 14 syl2anc AWordVBWordVNL+1L+MA++BprefixN=A++Bsubstr0N
16 3simpa AWordVBWordVNL+1L+MAWordVBWordV
17 6 3ad2ant1 AWordVBWordVNL+1L+ML0
18 0elfz L000L
19 17 18 syl AWordVBWordVNL+1L+M00L
20 5 nn0zd AWordVA
21 1 20 eqeltrid AWordVL
22 21 adantr AWordVBWordVL
23 uzid LLL
24 22 23 syl AWordVBWordVLL
25 peano2uz LLL+1L
26 fzss1 L+1LL+1L+MLL+M
27 24 25 26 3syl AWordVBWordVL+1L+MLL+M
28 2 eqcomi B=M
29 28 oveq2i L+B=L+M
30 29 oveq2i LL+B=LL+M
31 27 30 sseqtrrdi AWordVBWordVL+1L+MLL+B
32 31 sseld AWordVBWordVNL+1L+MNLL+B
33 32 3impia AWordVBWordVNL+1L+MNLL+B
34 19 33 jca AWordVBWordVNL+1L+M00LNLL+B
35 1 pfxccatin12 AWordVBWordV00LNLL+BA++Bsubstr0N=Asubstr0L++BprefixNL
36 16 34 35 sylc AWordVBWordVNL+1L+MA++Bsubstr0N=Asubstr0L++BprefixNL
37 1 opeq2i 0L=0A
38 37 oveq2i Asubstr0L=Asubstr0A
39 pfxval AWordVA0AprefixA=Asubstr0A
40 5 39 mpdan AWordVAprefixA=Asubstr0A
41 pfxid AWordVAprefixA=A
42 40 41 eqtr3d AWordVAsubstr0A=A
43 38 42 eqtrid AWordVAsubstr0L=A
44 43 3ad2ant1 AWordVBWordVNL+1L+MAsubstr0L=A
45 44 oveq1d AWordVBWordVNL+1L+MAsubstr0L++BprefixNL=A++BprefixNL
46 15 36 45 3eqtrd AWordVBWordVNL+1L+MA++BprefixN=A++BprefixNL