Metamath Proof Explorer

Theorem cshf1o

Description: Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023)

Ref Expression
Assertion cshf1o 
|- ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : dom W -1-1-onto-> ran W )

Proof

Step Hyp Ref Expression
1 cshwrnid 
 |-  ( ( W e. Word D /\ N e. ZZ ) -> ran ( W cyclShift N ) = ran W )
2 1 3adant2 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ran ( W cyclShift N ) = ran W )
3 wrddm 
 |-  ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
4 3 3ad2ant1 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> dom W = ( 0 ..^ ( # ` W ) ) )
5 simp2 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> W : dom W -1-1-> D )
6 f1eq2 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( W : dom W -1-1-> D <-> W : ( 0 ..^ ( # ` W ) ) -1-1-> D ) )
7 6 biimpa 
 |-  ( ( dom W = ( 0 ..^ ( # ` W ) ) /\ W : dom W -1-1-> D ) -> W : ( 0 ..^ ( # ` W ) ) -1-1-> D )
8 4 5 7 syl2anc 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> W : ( 0 ..^ ( # ` W ) ) -1-1-> D )
9 simp3 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> N e. ZZ )
10 eqid 
 |-  ( W cyclShift N ) = ( W cyclShift N )
11 cshf1 
 |-  ( ( W : ( 0 ..^ ( # ` W ) ) -1-1-> D /\ N e. ZZ /\ ( W cyclShift N ) = ( W cyclShift N ) ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) -1-1-> D )
12 10 11 mp3an3 
 |-  ( ( W : ( 0 ..^ ( # ` W ) ) -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) -1-1-> D )
13 8 9 12 syl2anc 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) -1-1-> D )
14 f1eq2 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( W cyclShift N ) : dom W -1-1-> D <-> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) -1-1-> D ) )
15 14 biimpar 
 |-  ( ( dom W = ( 0 ..^ ( # ` W ) ) /\ ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) -1-1-> D ) -> ( W cyclShift N ) : dom W -1-1-> D )
16 4 13 15 syl2anc 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : dom W -1-1-> D )
17 f1f1orn 
 |-  ( ( W cyclShift N ) : dom W -1-1-> D -> ( W cyclShift N ) : dom W -1-1-onto-> ran ( W cyclShift N ) )
18 16 17 syl 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : dom W -1-1-onto-> ran ( W cyclShift N ) )
19 f1oeq3 
 |-  ( ran ( W cyclShift N ) = ran W -> ( ( W cyclShift N ) : dom W -1-1-onto-> ran ( W cyclShift N ) <-> ( W cyclShift N ) : dom W -1-1-onto-> ran W ) )
20 19 biimpa 
 |-  ( ( ran ( W cyclShift N ) = ran W /\ ( W cyclShift N ) : dom W -1-1-onto-> ran ( W cyclShift N ) ) -> ( W cyclShift N ) : dom W -1-1-onto-> ran W )
21 2 18 20 syl2anc 
 |-  ( ( W e. Word D /\ W : dom W -1-1-> D /\ N e. ZZ ) -> ( W cyclShift N ) : dom W -1-1-onto-> ran W )