Metamath Proof Explorer

Theorem pfxlen

Description: Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

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

Proof

Step Hyp Ref Expression
1 pfxfn 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) Fn ( 0 ..^ L ) )
2 hashfn 
 |-  ( ( S prefix L ) Fn ( 0 ..^ L ) -> ( # ` ( S prefix L ) ) = ( # ` ( 0 ..^ L ) ) )
3 1 2 syl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix L ) ) = ( # ` ( 0 ..^ L ) ) )
4 elfznn0 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> L e. NN0 )
5 4 adantl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> L e. NN0 )
6 hashfzo0 
 |-  ( L e. NN0 -> ( # ` ( 0 ..^ L ) ) = L )
7 5 6 syl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( 0 ..^ L ) ) = L )
8 3 7 eqtrd 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix L ) ) = L )