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 \in Word V \land N \in (0 \dots \|W\|)) \to (W prefix N) prefix N = W prefix N$

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ N \in (0 \dots \|W\|) \to N \in ℕ_{0}$
2		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
3	1 2	sylib	$⊢ N \in (0 \dots \|W\|) \to N \in (0 \dots N)$
4	3	adantl	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to N \in (0 \dots N)$
5		pfxpfx	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land N \in (0 \dots N)) \to (W prefix N) prefix N = W prefix N$
6	4 5	mpd3an3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|)) \to (W prefix N) prefix N = W prefix N$

Metamath Proof Explorer

Theorem pfxpfxid

Proof