Metamath Proof Explorer

Theorem redwlklem

Description: Lemma for redwlk . (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion redwlklem 
|- ( ( F e. Word S /\ 1 <_ ( # ` F ) /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> V )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( F e. Word S /\ 1 <_ ( # ` F ) ) /\ P : ( 0 ... ( # ` F ) ) --> V ) -> P : ( 0 ... ( # ` F ) ) --> V )
2 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
3 fssres 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ..^ ( # ` F ) ) --> V )
4 1 2 3 sylancl 
 |-  ( ( ( F e. Word S /\ 1 <_ ( # ` F ) ) /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ..^ ( # ` F ) ) --> V )
5 4 ex 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ..^ ( # ` F ) ) --> V ) )
6 lencl 
 |-  ( F e. Word S -> ( # ` F ) e. NN0 )
7 6 nn0zd 
 |-  ( F e. Word S -> ( # ` F ) e. ZZ )
8 fzoval 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
9 7 8 syl 
 |-  ( F e. Word S -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
10 9 adantr 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
11 wrdred1hash 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )
12 oveq2 
 |-  ( ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) -> ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
13 12 eqeq2d 
 |-  ( ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) -> ( ( 0 ..^ ( # ` F ) ) = ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) <-> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) ) )
14 11 13 syl 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( ( 0 ..^ ( # ` F ) ) = ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) <-> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) ) )
15 10 14 mpbird 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) )
16 15 feq2d 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ..^ ( # ` F ) ) --> V <-> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> V ) )
17 5 16 sylibd 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> V ) )
18 17 3impia 
 |-  ( ( F e. Word S /\ 1 <_ ( # ` F ) /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( P |` ( 0 ..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ) ) --> V )