This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshwn

Description: A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshwn 
|- ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )

Proof

Step Hyp Ref Expression
1 0csh0 
 |-  ( (/) cyclShift ( # ` W ) ) = (/)
2 oveq1 
 |-  ( (/) = W -> ( (/) cyclShift ( # ` W ) ) = ( W cyclShift ( # ` W ) ) )
3 id 
 |-  ( (/) = W -> (/) = W )
4 1 2 3 3eqtr3a 
 |-  ( (/) = W -> ( W cyclShift ( # ` W ) ) = W )
5 4 a1d 
 |-  ( (/) = W -> ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W ) )
6 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
7 6 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
8 cshwmodn 
 |-  ( ( W e. Word V /\ ( # ` W ) e. ZZ ) -> ( W cyclShift ( # ` W ) ) = ( W cyclShift ( ( # ` W ) mod ( # ` W ) ) ) )
9 7 8 mpdan 
 |-  ( W e. Word V -> ( W cyclShift ( # ` W ) ) = ( W cyclShift ( ( # ` W ) mod ( # ` W ) ) ) )
10 9 adantl 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift ( # ` W ) ) = ( W cyclShift ( ( # ` W ) mod ( # ` W ) ) ) )
11 necom 
 |-  ( (/) =/= W <-> W =/= (/) )
12 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
13 11 12 sylan2b 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( # ` W ) e. NN )
14 13 nnrpd 
 |-  ( ( W e. Word V /\ (/) =/= W ) -> ( # ` W ) e. RR+ )
15 14 ancoms 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( # ` W ) e. RR+ )
16 modid0 
 |-  ( ( # ` W ) e. RR+ -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
17 15 16 syl 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( ( # ` W ) mod ( # ` W ) ) = 0 )
18 17 oveq2d 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift ( ( # ` W ) mod ( # ` W ) ) ) = ( W cyclShift 0 ) )
19 cshw0 
 |-  ( W e. Word V -> ( W cyclShift 0 ) = W )
20 19 adantl 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift 0 ) = W )
21 10 18 20 3eqtrd 
 |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift ( # ` W ) ) = W )
22 21 ex 
 |-  ( (/) =/= W -> ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W ) )
23 5 22 pm2.61ine 
 |-  ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )