Theorem pfxwrdsymb

Description: A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022)

	Ref	Expression
Assertion	pfxwrdsymb	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) ∈ Word ( 𝑆 “ ( 0 ..^ 𝐿 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pfxval0	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) = ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) )
2		swrdwrdsymb	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 0 , 𝐿 ⟩ ) ∈ Word ( 𝑆 “ ( 0 ..^ 𝐿 ) ) )
3	1 2	eqeltrd	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐿 ) ∈ Word ( 𝑆 “ ( 0 ..^ 𝐿 ) ) )