Metamath Proof Explorer

Theorem wrdred1hash

Description: The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion wrdred1hash 
|- ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( F e. Word S -> ( # ` F ) e. NN0 )
2 wrdf 
 |-  ( F e. Word S -> F : ( 0 ..^ ( # ` F ) ) --> S )
3 ffn 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> S -> F Fn ( 0 ..^ ( # ` F ) ) )
4 nn0z 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
5 fzossrbm1 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
6 4 5 syl 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
7 6 adantr 
 |-  ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
8 7 adantl 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
9 fnssresb 
 |-  ( F Fn ( 0 ..^ ( # ` F ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) Fn ( 0 ..^ ( ( # ` F ) - 1 ) ) <-> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) ) )
10 9 adantr 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) Fn ( 0 ..^ ( ( # ` F ) - 1 ) ) <-> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) ) )
11 8 10 mpbird 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) Fn ( 0 ..^ ( ( # ` F ) - 1 ) ) )
12 hashfn 
 |-  ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) Fn ( 0 ..^ ( ( # ` F ) - 1 ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( # ` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) )
13 11 12 syl 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( # ` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) )
14 1nn0 
 |-  1 e. NN0
15 nn0sub2 
 |-  ( ( 1 e. NN0 /\ ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. NN0 )
16 14 15 mp3an1 
 |-  ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. NN0 )
17 hashfzo0 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> ( # ` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) = ( ( # ` F ) - 1 ) )
18 16 17 syl 
 |-  ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( # ` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) = ( ( # ` F ) - 1 ) )
19 18 adantl 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( # ` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) = ( ( # ` F ) - 1 ) )
20 13 19 eqtrd 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )
21 20 ex 
 |-  ( F Fn ( 0 ..^ ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) )
22 2 3 21 3syl 
 |-  ( F e. Word S -> ( ( ( # ` F ) e. NN0 /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) )
23 1 22 mpand 
 |-  ( F e. Word S -> ( 1 <_ ( # ` F ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) ) )
24 23 imp 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )