Metamath Proof Explorer

Theorem swrdlen

Description: Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion swrdlen 
|- ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( S ` ( x + F ) ) e. _V
2 eqid 
 |-  ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) )
3 1 2 fnmpti 
 |-  ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) Fn ( 0 ..^ ( L - F ) )
4 swrdval2 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )
5 4 fneq1d 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) Fn ( 0 ..^ ( L - F ) ) <-> ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) Fn ( 0 ..^ ( L - F ) ) ) )
6 3 5 mpbiri 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) Fn ( 0 ..^ ( L - F ) ) )
7 hashfn 
 |-  ( ( S substr <. F , L >. ) Fn ( 0 ..^ ( L - F ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( # ` ( 0 ..^ ( L - F ) ) ) )
8 6 7 syl 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( # ` ( 0 ..^ ( L - F ) ) ) )
9 fznn0sub 
 |-  ( F e. ( 0 ... L ) -> ( L - F ) e. NN0 )
10 9 3ad2ant2 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( L - F ) e. NN0 )
11 hashfzo0 
 |-  ( ( L - F ) e. NN0 -> ( # ` ( 0 ..^ ( L - F ) ) ) = ( L - F ) )
12 10 11 syl 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( 0 ..^ ( L - F ) ) ) = ( L - F ) )
13 8 12 eqtrd 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. F , L >. ) ) = ( L - F ) )