Metamath Proof Explorer


Theorem cshwmodn

Description: Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

Ref Expression
Assertion cshwmodn W Word V N W cyclShift N = W cyclShift N mod W

Proof

Step Hyp Ref Expression
1 0csh0 cyclShift N =
2 oveq1 W = W cyclShift N = cyclShift N
3 oveq1 W = W cyclShift N mod W = cyclShift N mod W
4 0csh0 cyclShift N mod W =
5 3 4 syl6eq W = W cyclShift N mod W =
6 1 2 5 3eqtr4a W = W cyclShift N = W cyclShift N mod W
7 6 a1d W = W Word V N W cyclShift N = W cyclShift N mod W
8 lennncl W Word V W W
9 8 ex W Word V W W
10 9 adantr W Word V N W W
11 10 impcom W W Word V N W
12 simprr W W Word V N N
13 zre N N
14 nnrp W W +
15 modabs2 N W + N mod W mod W = N mod W
16 13 14 15 syl2anr W N N mod W mod W = N mod W
17 16 opeq1d W N N mod W mod W W = N mod W W
18 17 oveq2d W N W substr N mod W mod W W = W substr N mod W W
19 16 oveq2d W N W prefix N mod W mod W = W prefix N mod W
20 18 19 oveq12d W N W substr N mod W mod W W ++ W prefix N mod W mod W = W substr N mod W W ++ W prefix N mod W
21 11 12 20 syl2anc W W Word V N W substr N mod W mod W W ++ W prefix N mod W mod W = W substr N mod W W ++ W prefix N mod W
22 simprl W W Word V N W Word V
23 12 11 zmodcld W W Word V N N mod W 0
24 23 nn0zd W W Word V N N mod W
25 cshword W Word V N mod W W cyclShift N mod W = W substr N mod W mod W W ++ W prefix N mod W mod W
26 22 24 25 syl2anc W W Word V N W cyclShift N mod W = W substr N mod W mod W W ++ W prefix N mod W mod W
27 cshword W Word V N W cyclShift N = W substr N mod W W ++ W prefix N mod W
28 27 adantl W W Word V N W cyclShift N = W substr N mod W W ++ W prefix N mod W
29 21 26 28 3eqtr4rd W W Word V N W cyclShift N = W cyclShift N mod W
30 29 ex W W Word V N W cyclShift N = W cyclShift N mod W
31 7 30 pm2.61ine W Word V N W cyclShift N = W cyclShift N mod W