Metamath Proof Explorer


Theorem pfxswrd

Description: A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018) (Revised by AV, 8-May-2020)

Ref Expression
Assertion pfxswrd WWordVN0WM0NL0NMWsubstrMNprefixL=WsubstrMM+L

Proof

Step Hyp Ref Expression
1 ovexd WWordVN0WM0NWsubstrMNV
2 elfznn0 L0NML0
3 pfxval WsubstrMNVL0WsubstrMNprefixL=WsubstrMNsubstr0L
4 1 2 3 syl2an WWordVN0WM0NL0NMWsubstrMNprefixL=WsubstrMNsubstr0L
5 fznn0sub M0NNM0
6 5 3ad2ant3 WWordVN0WM0NNM0
7 0elfz NM000NM
8 6 7 syl WWordVN0WM0N00NM
9 8 anim1i WWordVN0WM0NL0NM00NML0NM
10 swrdswrd WWordVN0WM0N00NML0NMWsubstrMNsubstr0L=WsubstrM+0M+L
11 10 imp WWordVN0WM0N00NML0NMWsubstrMNsubstr0L=WsubstrM+0M+L
12 9 11 syldan WWordVN0WM0NL0NMWsubstrMNsubstr0L=WsubstrM+0M+L
13 elfznn0 M0NM0
14 nn0cn M0M
15 14 addid1d M0M+0=M
16 13 15 syl M0NM+0=M
17 16 3ad2ant3 WWordVN0WM0NM+0=M
18 17 adantr WWordVN0WM0NL0NMM+0=M
19 18 opeq1d WWordVN0WM0NL0NMM+0M+L=MM+L
20 19 oveq2d WWordVN0WM0NL0NMWsubstrM+0M+L=WsubstrMM+L
21 4 12 20 3eqtrd WWordVN0WM0NL0NMWsubstrMNprefixL=WsubstrMM+L
22 21 ex WWordVN0WM0NL0NMWsubstrMNprefixL=WsubstrMM+L