Metamath Proof Explorer

Theorem pfxres

Description: Value of the subword extractor for left-anchored subwords. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxres 
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( S |` ( 0 ..^ L ) ) )

Proof

Step Hyp Ref Expression
1 pfxmpt 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( x e. ( 0 ..^ L ) |-> ( S ` x ) ) )
2 wrdf 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> A )
3 2 adantr 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> S : ( 0 ..^ ( # ` S ) ) --> A )
4 elfzuz3 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` L ) )
5 4 adantl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` S ) e. ( ZZ>= ` L ) )
6 fzoss2 
 |-  ( ( # ` S ) e. ( ZZ>= ` L ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` S ) ) )
7 5 6 syl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` S ) ) )
8 3 7 feqresmpt 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S |` ( 0 ..^ L ) ) = ( x e. ( 0 ..^ L ) |-> ( S ` x ) ) )
9 1 8 eqtr4d 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( S |` ( 0 ..^ L ) ) )