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 ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 1nn0 1 ∈ ℕ0
2 1 a1i ( 𝑊 ≠ ∅ → 1 ∈ ℕ0 )
3 pfxval ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ℕ0 ) → ( 𝑊 prefix 1 ) = ( 𝑊 substr ⟨ 0 , 1 ⟩ ) )
4 2 3 sylan2 ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = ( 𝑊 substr ⟨ 0 , 1 ⟩ ) )
5 1e0p1 1 = ( 0 + 1 )
6 5 opeq2i ⟨ 0 , 1 ⟩ = ⟨ 0 , ( 0 + 1 ) ⟩
7 6 oveq2i ( 𝑊 substr ⟨ 0 , 1 ⟩ ) = ( 𝑊 substr ⟨ 0 , ( 0 + 1 ) ⟩ )
8 7 a1i ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 substr ⟨ 0 , 1 ⟩ ) = ( 𝑊 substr ⟨ 0 , ( 0 + 1 ) ⟩ ) )
9 lennncl ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
10 lbfzo0 ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
11 9 10 sylibr ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 swrds1 ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 0 , ( 0 + 1 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
13 11 12 syldan ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 substr ⟨ 0 , ( 0 + 1 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
14 4 8 13 3eqtrd ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )