Metamath Proof Explorer

Theorem 1cshid

Description: Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 cshwmodn 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
2 1 3adant3 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
3 simp3 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( # ` W ) = 1 )
4 3 oveq2d 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( N mod ( # ` W ) ) = ( N mod 1 ) )
5 zmod10 
 |-  ( N e. ZZ -> ( N mod 1 ) = 0 )
6 5 3ad2ant2 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( N mod 1 ) = 0 )
7 4 6 eqtrd 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( N mod ( # ` W ) ) = 0 )
8 7 oveq2d 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( W cyclShift ( N mod ( # ` W ) ) ) = ( W cyclShift 0 ) )
9 cshw0 
 |-  ( W e. Word V -> ( W cyclShift 0 ) = W )
10 9 3ad2ant1 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( W cyclShift 0 ) = W )
11 2 8 10 3eqtrd 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( # ` W ) = 1 ) -> ( W cyclShift N ) = W )