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

Metamath Proof Explorer

Theorem pfxres

Description: Value of the prefix extractor as the restriction of a word. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxres ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 ↾ ( 0 ..^ 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 pfxmpt ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑆 ‘ 𝑥 ) ) )
2 wrdf ⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
3 2 adantr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
4 elfzuz3 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
5 4 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
6 fzoss2 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
7 5 6 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 0 ..^ 𝐿 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
8 3 7 feqresmpt ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ↾ ( 0 ..^ 𝐿 ) ) = ( 𝑥 ∈ ( 0 ..^ 𝐿 ) ↦ ( 𝑆 ‘ 𝑥 ) ) )
9 1 8 eqtr4d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) = ( 𝑆 ↾ ( 0 ..^ 𝐿 ) ) )