Metamath Proof Explorer


Theorem pfxccatpfx1

Description: A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020)

Ref Expression
Hypothesis swrdccatin2.l L=A
Assertion pfxccatpfx1 AWordVBWordVN0LA++BprefixN=AprefixN

Proof

Step Hyp Ref Expression
1 swrdccatin2.l L=A
2 3simpa AWordVBWordVN0LAWordVBWordV
3 elfznn0 N0LN0
4 0elfz N000N
5 3 4 syl N0L00N
6 1 oveq2i 0L=0A
7 6 eleq2i N0LN0A
8 7 biimpi N0LN0A
9 5 8 jca N0L00NN0A
10 9 3ad2ant3 AWordVBWordVN0L00NN0A
11 swrdccatin1 AWordVBWordV00NN0AA++Bsubstr0N=Asubstr0N
12 2 10 11 sylc AWordVBWordVN0LA++Bsubstr0N=Asubstr0N
13 ccatcl AWordVBWordVA++BWordV
14 13 3adant3 AWordVBWordVN0LA++BWordV
15 3 3ad2ant3 AWordVBWordVN0LN0
16 14 15 jca AWordVBWordVN0LA++BWordVN0
17 pfxval A++BWordVN0A++BprefixN=A++Bsubstr0N
18 16 17 syl AWordVBWordVN0LA++BprefixN=A++Bsubstr0N
19 pfxval AWordVN0AprefixN=Asubstr0N
20 3 19 sylan2 AWordVN0LAprefixN=Asubstr0N
21 20 3adant2 AWordVBWordVN0LAprefixN=Asubstr0N
22 12 18 21 3eqtr4d AWordVBWordVN0LA++BprefixN=AprefixN