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 ..^ 𝐿 ) ) )