Metamath Proof Explorer


Theorem pfxpfxid

Description: A prefix of a prefix with the same length is the original prefix. In other words, the operation "prefix of length N " is idempotent. (Contributed by AV, 5-Apr-2018) (Revised by AV, 8-May-2020)

Ref Expression
Assertion pfxpfxid WWordVN0WWprefixNprefixN=WprefixN

Proof

Step Hyp Ref Expression
1 elfznn0 N0WN0
2 nn0fz0 N0N0N
3 1 2 sylib N0WN0N
4 3 adantl WWordVN0WN0N
5 pfxpfx WWordVN0WN0NWprefixNprefixN=WprefixN
6 4 5 mpd3an3 WWordVN0WWprefixNprefixN=WprefixN