Metamath Proof Explorer

Theorem ccat2s1p1

Description: Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 20-Jan-2024)

		Ref	Expression
	Assertion	ccat2s1p1	$⊢ X \in V \to (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) (0) = X$

Proof

Step	Hyp	Ref	Expression
1		s1cli	$⊢ ⟨“ X ”⟩ \in Word V$
2		s1cli	$⊢ ⟨“ Y ”⟩ \in Word V$
3		s1len	$⊢ \|⟨“ X ”⟩\| = 1$
4		1nn	$⊢ 1 \in ℕ$
5	3 4	eqeltri	$⊢ \|⟨“ X ”⟩\| \in ℕ$
6		lbfzo0	$⊢ 0 \in (0 ..^\|⟨“ X ”⟩\|) \leftrightarrow \|⟨“ X ”⟩\| \in ℕ$
7	5 6	mpbir	$⊢ 0 \in (0 ..^\|⟨“ X ”⟩\|)$
8		ccatval1	$⊢ (⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V \land 0 \in (0 ..^\|⟨“ X ”⟩\|)) \to (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) (0) = ⟨“ X ”⟩ (0)$
9	1 2 7 8	mp3an	$⊢ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) (0) = ⟨“ X ”⟩ (0)$
10		s1fv	$⊢ X \in V \to ⟨“ X ”⟩ (0) = X$
11	9 10	eqtrid	$⊢ X \in V \to (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) (0) = X$