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