Metamath Proof Explorer

Theorem 2cshwid

Description: Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018) (Revised by AV, 5-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion 2cshwid 
|- ( ( W e. Word V /\ N e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( ( # ` W ) - N ) ) = W )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
2 1 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
3 zsubcl 
 |-  ( ( ( # ` W ) e. ZZ /\ N e. ZZ ) -> ( ( # ` W ) - N ) e. ZZ )
4 2 3 sylan 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( ( # ` W ) - N ) e. ZZ )
5 2cshw 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( ( # ` W ) - N ) e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( ( # ` W ) - N ) ) = ( W cyclShift ( N + ( ( # ` W ) - N ) ) ) )
6 4 5 mpd3an3 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( ( # ` W ) - N ) ) = ( W cyclShift ( N + ( ( # ` W ) - N ) ) ) )
7 zcn 
 |-  ( N e. ZZ -> N e. CC )
8 1 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
9 pncan3 
 |-  ( ( N e. CC /\ ( # ` W ) e. CC ) -> ( N + ( ( # ` W ) - N ) ) = ( # ` W ) )
10 7 8 9 syl2anr 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( N + ( ( # ` W ) - N ) ) = ( # ` W ) )
11 10 oveq2d 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift ( N + ( ( # ` W ) - N ) ) ) = ( W cyclShift ( # ` W ) ) )
12 cshwn 
 |-  ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )
13 12 adantr 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift ( # ` W ) ) = W )
14 6 11 13 3eqtrd 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( ( # ` W ) - N ) ) = W )