Metamath Proof Explorer


Theorem pfxf

Description: A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxf ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝑉 )

Proof

Step Hyp Ref Expression
1 pfxmpt ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑊𝑥 ) ) )
2 simpll ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑊 ∈ Word 𝑉 )
3 elfzuz3 ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝐿 ) )
4 3 adantl ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝐿 ) )
5 fzoss2 ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ𝐿 ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 4 5 syl ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7 6 sselda ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
8 wrdsymbcl ( ( 𝑊 ∈ Word 𝑉𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊𝑥 ) ∈ 𝑉 )
9 2 7 8 syl2anc ( ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑊𝑥 ) ∈ 𝑉 )
10 1 9 fmpt3d ( ( 𝑊 ∈ Word 𝑉𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝑉 )