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