Metamath Proof Explorer

Theorem pfxcctswrd

Description: The concatenation of the prefix of a word and the rest of the word yields the word itself. (Contributed by AV, 21-Oct-2018) (Revised by AV, 9-May-2020)

		Ref	Expression
	Assertion	pfxcctswrd	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to (W prefix M) ++ (W substr ⟨M, \|W\|⟩) = W$

Proof

Step	Hyp	Ref	Expression
1		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
2		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
3	1 2	sylib	$⊢ W \in Word V \to \|W\| \in (0 \dots \|W\|)$
4	3	adantr	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W\| \in (0 \dots \|W\|)$
5		ccatpfx	$⊢ (W \in Word V \land M \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to (W prefix M) ++ (W substr ⟨M, \|W\|⟩) = W prefix \|W\|$
6	4 5	mpd3an3	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to (W prefix M) ++ (W substr ⟨M, \|W\|⟩) = W prefix \|W\|$
7		pfxid	$⊢ W \in Word V \to W prefix \|W\| = W$
8	7	adantr	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to W prefix \|W\| = W$
9	6 8	eqtrd	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to (W prefix M) ++ (W substr ⟨M, \|W\|⟩) = W$