Metamath Proof Explorer

Theorem cshwf

Description: A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018)

Ref Expression
Assertion cshwf 
|- ( ( W e. Word A /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) --> A )

Proof

Step Hyp Ref Expression
1 cshwcl 
 |-  ( W e. Word A -> ( W cyclShift N ) e. Word A )
2 wrdf 
 |-  ( ( W cyclShift N ) e. Word A -> ( W cyclShift N ) : ( 0 ..^ ( # ` ( W cyclShift N ) ) ) --> A )
3 1 2 syl 
 |-  ( W e. Word A -> ( W cyclShift N ) : ( 0 ..^ ( # ` ( W cyclShift N ) ) ) --> A )
4 3 adantr 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` ( W cyclShift N ) ) ) --> A )
5 cshwlen 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
6 5 oveq2d 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( 0 ..^ ( # ` ( W cyclShift N ) ) ) = ( 0 ..^ ( # ` W ) ) )
7 6 feq2d 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( ( W cyclShift N ) : ( 0 ..^ ( # ` ( W cyclShift N ) ) ) --> A <-> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) --> A ) )
8 4 7 mpbid 
 |-  ( ( W e. Word A /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) --> A )