# 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 ) ) ) )`
` |-  ( ( (/) =/= 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 )`
` |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift 0 ) = W )`
` |-  ( ( (/) =/= W /\ W e. Word V ) -> ( W cyclShift ( # ` W ) ) = W )`
` |-  ( (/) =/= W -> ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W ) )`
` |-  ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )`