This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. NN0 )
2 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
3 1 2 sylib 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. ( 0 ... N ) )
4 3 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> N e. ( 0 ... N ) )
5 pfxpfx 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ N e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )
6 4 5 mpd3an3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )