Description: Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | 3cshw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cshwid | |
|
2 | 1 | 3adant2 | |
3 | 2 | eqcomd | |
4 | 3 | oveq1d | |
5 | cshwcl | |
|
6 | 5 | 3ad2ant1 | |
7 | lencl | |
|
8 | 7 | nn0zd | |
9 | zsubcl | |
|
10 | 8 9 | sylan | |
11 | 10 | 3adant2 | |
12 | simp2 | |
|
13 | 2cshwcom | |
|
14 | 6 11 12 13 | syl3anc | |
15 | 4 14 | eqtrd | |