pfx1

Description: The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020)

		Ref	Expression
	Assertion	pfx1	$⊢ (W \in Word V \land W \neq \emptyset) \to W prefix 1 = ⟨“ W (0) ”⟩$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2	1	a1i	$⊢ W \neq \emptyset \to 1 \in ℕ_{0}$
3		pfxval	$⊢ (W \in Word V \land 1 \in ℕ_{0}) \to W prefix 1 = W substr ⟨0, 1⟩$
4	2 3	sylan2	$⊢ (W \in Word V \land W \neq \emptyset) \to W prefix 1 = W substr ⟨0, 1⟩$
5		1e0p1	$⊢ 1 = 0 + 1$
6	5	opeq2i	$⊢ ⟨0, 1⟩ = ⟨0, 0 + 1⟩$
7	6	oveq2i	$⊢ W substr ⟨0, 1⟩ = W substr ⟨0, 0 + 1⟩$
8	7	a1i	$⊢ (W \in Word V \land W \neq \emptyset) \to W substr ⟨0, 1⟩ = W substr ⟨0, 0 + 1⟩$
9		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
10		lbfzo0	$⊢ 0 \in (0 ..^\|W\|) \leftrightarrow \|W\| \in ℕ$
11	9 10	sylibr	$⊢ (W \in Word V \land W \neq \emptyset) \to 0 \in (0 ..^\|W\|)$
12		swrds1	$⊢ (W \in Word V \land 0 \in (0 ..^\|W\|)) \to W substr ⟨0, 0 + 1⟩ = ⟨“ W (0) ”⟩$
13	11 12	syldan	$⊢ (W \in Word V \land W \neq \emptyset) \to W substr ⟨0, 0 + 1⟩ = ⟨“ W (0) ”⟩$
14	4 8 13	3eqtrd	$⊢ (W \in Word V \land W \neq \emptyset) \to W prefix 1 = ⟨“ W (0) ”⟩$

Metamath Proof Explorer