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 ) )