This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ”⟩ )