Metamath Proof Explorer

Theorem cshinj

Description: If a word is injectiv (regarded as function), the cyclically shifted word is also injective. (Contributed by AV, 14-Mar-2021)

Ref Expression
Assertion cshinj 
|- ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) -> ( G = ( F cyclShift S ) -> Fun `' G ) )

Proof

Step Hyp Ref Expression
1 wrdf 
 |-  ( F e. Word A -> F : ( 0 ..^ ( # ` F ) ) --> A )
2 df-f1 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A <-> ( F : ( 0 ..^ ( # ` F ) ) --> A /\ Fun `' F ) )
3 2 biimpri 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> A /\ Fun `' F ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> A )
4 1 3 sylan 
 |-  ( ( F e. Word A /\ Fun `' F ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> A )
5 4 3adant3 
 |-  ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> A )
6 5 adantr 
 |-  ( ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> A )
7 simpl3 
 |-  ( ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> S e. ZZ )
8 simpr 
 |-  ( ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> G = ( F cyclShift S ) )
9 cshf1 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> A /\ S e. ZZ /\ G = ( F cyclShift S ) ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> A )
10 6 7 8 9 syl3anc 
 |-  ( ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) /\ G = ( F cyclShift S ) ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> A )
11 10 ex 
 |-  ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) -> ( G = ( F cyclShift S ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> A ) )
12 df-f1 
 |-  ( G : ( 0 ..^ ( # ` F ) ) -1-1-> A <-> ( G : ( 0 ..^ ( # ` F ) ) --> A /\ Fun `' G ) )
13 12 simprbi 
 |-  ( G : ( 0 ..^ ( # ` F ) ) -1-1-> A -> Fun `' G )
14 11 13 syl6 
 |-  ( ( F e. Word A /\ Fun `' F /\ S e. ZZ ) -> ( G = ( F cyclShift S ) -> Fun `' G ) )