Metamath Proof Explorer

Theorem cshwsublen

Description: Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( # ` W ) = 0 -> ( N - ( # ` W ) ) = ( N - 0 ) )
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 2 subid1d 
 |-  ( N e. ZZ -> ( N - 0 ) = N )
4 3 adantl 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( N - 0 ) = N )
5 1 4 sylan9eq 
 |-  ( ( ( # ` W ) = 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( N - ( # ` W ) ) = N )
6 5 eqcomd 
 |-  ( ( ( # ` W ) = 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> N = ( N - ( # ` W ) ) )
7 6 oveq2d 
 |-  ( ( ( # ` W ) = 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) )
8 7 ex 
 |-  ( ( # ` W ) = 0 -> ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) ) )
9 zre 
 |-  ( N e. ZZ -> N e. RR )
10 9 adantl 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> N e. RR )
11 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
12 elnnne0 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) )
13 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
14 12 13 sylbir 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> ( # ` W ) e. RR+ )
15 14 ex 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) =/= 0 -> ( # ` W ) e. RR+ ) )
16 11 15 syl 
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 -> ( # ` W ) e. RR+ ) )
17 16 adantr 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( ( # ` W ) =/= 0 -> ( # ` W ) e. RR+ ) )
18 17 impcom 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( # ` W ) e. RR+ )
19 modeqmodmin 
 |-  ( ( N e. RR /\ ( # ` W ) e. RR+ ) -> ( N mod ( # ` W ) ) = ( ( N - ( # ` W ) ) mod ( # ` W ) ) )
20 10 18 19 syl2an2 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( N mod ( # ` W ) ) = ( ( N - ( # ` W ) ) mod ( # ` W ) ) )
21 20 oveq2d 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift ( N mod ( # ` W ) ) ) = ( W cyclShift ( ( N - ( # ` W ) ) mod ( # ` W ) ) ) )
22 cshwmodn 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
23 22 adantl 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift N ) = ( W cyclShift ( N mod ( # ` W ) ) ) )
24 simpl 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> W e. Word V )
25 11 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
26 zsubcl 
 |-  ( ( N e. ZZ /\ ( # ` W ) e. ZZ ) -> ( N - ( # ` W ) ) e. ZZ )
27 25 26 sylan2 
 |-  ( ( N e. ZZ /\ W e. Word V ) -> ( N - ( # ` W ) ) e. ZZ )
28 27 ancoms 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( N - ( # ` W ) ) e. ZZ )
29 24 28 jca 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W e. Word V /\ ( N - ( # ` W ) ) e. ZZ ) )
30 29 adantl 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W e. Word V /\ ( N - ( # ` W ) ) e. ZZ ) )
31 cshwmodn 
 |-  ( ( W e. Word V /\ ( N - ( # ` W ) ) e. ZZ ) -> ( W cyclShift ( N - ( # ` W ) ) ) = ( W cyclShift ( ( N - ( # ` W ) ) mod ( # ` W ) ) ) )
32 30 31 syl 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift ( N - ( # ` W ) ) ) = ( W cyclShift ( ( N - ( # ` W ) ) mod ( # ` W ) ) ) )
33 21 23 32 3eqtr4d 
 |-  ( ( ( # ` W ) =/= 0 /\ ( W e. Word V /\ N e. ZZ ) ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) )
34 33 ex 
 |-  ( ( # ` W ) =/= 0 -> ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) ) )
35 8 34 pm2.61ine 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( W cyclShift ( N - ( # ` W ) ) ) )