Metamath Proof Explorer

Theorem wrdeqs1cat

Description: Decompose a nonempty word by separating off the first symbol. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 12-Oct-2022)

		Ref	Expression
	Assertion	wrdeqs1cat	$⊢ (W \in Word A \land W \neq \emptyset) \to W = ⟨“ W (0) ”⟩ ++ (W substr ⟨1, \|W\|⟩)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (W \in Word A \land W \neq \emptyset) \to W \in Word A$
2		wrdfin	$⊢ W \in Word A \to W \in Fin$
3		1elfz0hash	$⊢ (W \in Fin \land W \neq \emptyset) \to 1 \in (0 \dots \|W\|)$
4	2 3	sylan	$⊢ (W \in Word A \land W \neq \emptyset) \to 1 \in (0 \dots \|W\|)$
5		lennncl	$⊢ (W \in Word A \land W \neq \emptyset) \to \|W\| \in ℕ$
6	5	nnnn0d	$⊢ (W \in Word A \land W \neq \emptyset) \to \|W\| \in ℕ_{0}$
7		eluzfz2	$⊢ \|W\| \in ℤ_{\geq 0} \to \|W\| \in (0 \dots \|W\|)$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9	7 8	eleq2s	$⊢ \|W\| \in ℕ_{0} \to \|W\| \in (0 \dots \|W\|)$
10	6 9	syl	$⊢ (W \in Word A \land W \neq \emptyset) \to \|W\| \in (0 \dots \|W\|)$
11		ccatpfx	$⊢ (W \in Word A \land 1 \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to (W prefix 1) ++ (W substr ⟨1, \|W\|⟩) = W prefix \|W\|$
12	1 4 10 11	syl3anc	$⊢ (W \in Word A \land W \neq \emptyset) \to (W prefix 1) ++ (W substr ⟨1, \|W\|⟩) = W prefix \|W\|$
13		pfx1	$⊢ (W \in Word A \land W \neq \emptyset) \to W prefix 1 = ⟨“ W (0) ”⟩$
14	13	oveq1d	$⊢ (W \in Word A \land W \neq \emptyset) \to (W prefix 1) ++ (W substr ⟨1, \|W\|⟩) = ⟨“ W (0) ”⟩ ++ (W substr ⟨1, \|W\|⟩)$
15		pfxid	$⊢ W \in Word A \to W prefix \|W\| = W$
16	15	adantr	$⊢ (W \in Word A \land W \neq \emptyset) \to W prefix \|W\| = W$
17	12 14 16	3eqtr3rd	$⊢ (W \in Word A \land W \neq \emptyset) \to W = ⟨“ W (0) ”⟩ ++ (W substr ⟨1, \|W\|⟩)$