Metamath Proof Explorer


Theorem 3cshw

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 WWordVNMWcyclShiftN=WcyclShiftMcyclShiftNcyclShiftWM

Proof

Step Hyp Ref Expression
1 2cshwid WWordVMWcyclShiftMcyclShiftWM=W
2 1 3adant2 WWordVNMWcyclShiftMcyclShiftWM=W
3 2 eqcomd WWordVNMW=WcyclShiftMcyclShiftWM
4 3 oveq1d WWordVNMWcyclShiftN=WcyclShiftMcyclShiftWMcyclShiftN
5 cshwcl WWordVWcyclShiftMWordV
6 5 3ad2ant1 WWordVNMWcyclShiftMWordV
7 lencl WWordVW0
8 7 nn0zd WWordVW
9 zsubcl WMWM
10 8 9 sylan WWordVMWM
11 10 3adant2 WWordVNMWM
12 simp2 WWordVNMN
13 2cshwcom WcyclShiftMWordVWMNWcyclShiftMcyclShiftWMcyclShiftN=WcyclShiftMcyclShiftNcyclShiftWM
14 6 11 12 13 syl3anc WWordVNMWcyclShiftMcyclShiftWMcyclShiftN=WcyclShiftMcyclShiftNcyclShiftWM
15 4 14 eqtrd WWordVNMWcyclShiftN=WcyclShiftMcyclShiftNcyclShiftWM