Metamath Proof Explorer

Theorem ccatfv0

Description: The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018)

		Ref	Expression
	Assertion	ccatfv0	$⊢ (A \in Word V \land B \in Word V \land 0 < \|A\|) \to (A ++ B) (0) = A (0)$

Proof

Step	Hyp	Ref	Expression
1		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
2		elnnnn0b	$⊢ \|A\| \in ℕ \leftrightarrow (\|A\| \in ℕ_{0} \land 0 < \|A\|)$
3	2	biimpri	$⊢ (\|A\| \in ℕ_{0} \land 0 < \|A\|) \to \|A\| \in ℕ$
4	1 3	sylan	$⊢ (A \in Word V \land 0 < \|A\|) \to \|A\| \in ℕ$
5		lbfzo0	$⊢ 0 \in (0 ..^\|A\|) \leftrightarrow \|A\| \in ℕ$
6	4 5	sylibr	$⊢ (A \in Word V \land 0 < \|A\|) \to 0 \in (0 ..^\|A\|)$
7	6	3adant2	$⊢ (A \in Word V \land B \in Word V \land 0 < \|A\|) \to 0 \in (0 ..^\|A\|)$
8		ccatval1	$⊢ (A \in Word V \land B \in Word V \land 0 \in (0 ..^\|A\|)) \to (A ++ B) (0) = A (0)$
9	7 8	syld3an3	$⊢ (A \in Word V \land B \in Word V \land 0 < \|A\|) \to (A ++ B) (0) = A (0)$