Metamath Proof Explorer

Theorem pfxccatid

Description: A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 10-May-2020)

		Ref	Expression
	Assertion	pfxccatid	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to (A ++ B) prefix N = A$

Proof

Step	Hyp	Ref	Expression
1		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
2		nn0fz0	$⊢ \|A\| \in ℕ_{0} \leftrightarrow \|A\| \in (0 \dots \|A\|)$
3	1 2	sylib	$⊢ A \in Word V \to \|A\| \in (0 \dots \|A\|)$
4	3	3ad2ant1	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to \|A\| \in (0 \dots \|A\|)$
5		eleq1	$⊢ N = \|A\| \to (N \in (0 \dots \|A\|) \leftrightarrow \|A\| \in (0 \dots \|A\|))$
6	5	3ad2ant3	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to (N \in (0 \dots \|A\|) \leftrightarrow \|A\| \in (0 \dots \|A\|))$
7	4 6	mpbird	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to N \in (0 \dots \|A\|)$
8		eqid	$⊢ \|A\| = \|A\|$
9	8	pfxccatpfx1	$⊢ (A \in Word V \land B \in Word V \land N \in (0 \dots \|A\|)) \to (A ++ B) prefix N = A prefix N$
10	7 9	syld3an3	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to (A ++ B) prefix N = A prefix N$
11		oveq2	$⊢ N = \|A\| \to A prefix N = A prefix \|A\|$
12	11	3ad2ant3	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to A prefix N = A prefix \|A\|$
13		pfxid	$⊢ A \in Word V \to A prefix \|A\| = A$
14	13	3ad2ant1	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to A prefix \|A\| = A$
15	10 12 14	3eqtrd	$⊢ (A \in Word V \land B \in Word V \land N = \|A\|) \to (A ++ B) prefix N = A$