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 Word V N W = 1 W cyclShift N = W

Proof

Step Hyp Ref Expression
1 cshwmodn W Word V N W cyclShift N = W cyclShift N mod W
2 1 3adant3 W Word V N W = 1 W cyclShift N = W cyclShift N mod W
3 simp3 W Word V N W = 1 W = 1
4 3 oveq2d W Word V N W = 1 N mod W = N mod 1
5 zmod10 N N mod 1 = 0
6 5 3ad2ant2 W Word V N W = 1 N mod 1 = 0
7 4 6 eqtrd W Word V N W = 1 N mod W = 0
8 7 oveq2d W Word V N W = 1 W cyclShift N mod W = W cyclShift 0
9 cshw0 W Word V W cyclShift 0 = W
10 9 3ad2ant1 W Word V N W = 1 W cyclShift 0 = W
11 2 8 10 3eqtrd W Word V N W = 1 W cyclShift N = W