Metamath Proof Explorer

Theorem 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 ∈ Word V ∧ W ≠ ∅ → W prefix 1 = ⟨“ W ⁡ 0 ”⟩

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ 0
2 1 a1i ⊢ W ≠ ∅ → 1 ∈ ℕ 0
3 pfxval ⊢ W ∈ Word V ∧ 1 ∈ ℕ 0 → W prefix 1 = W substr 0 1
4 2 3 sylan2 ⊢ W ∈ Word V ∧ W ≠ ∅ → 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 ∈ Word V ∧ W ≠ ∅ → W substr 0 1 = W substr 0 0 + 1
9 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
10 lbfzo0 ⊢ 0 ∈ 0 ..^ W ↔ W ∈ ℕ
11 9 10 sylibr ⊢ W ∈ Word V ∧ W ≠ ∅ → 0 ∈ 0 ..^ W
12 swrds1 ⊢ W ∈ Word V ∧ 0 ∈ 0 ..^ W → W substr 0 0 + 1 = ⟨“ W ⁡ 0 ”⟩
13 11 12 syldan ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr 0 0 + 1 = ⟨“ W ⁡ 0 ”⟩
14 4 8 13 3eqtrd ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix 1 = ⟨“ W ⁡ 0 ”⟩