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∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W

Proof

Step Hyp Ref Expression
1 oveq2 ⊢W=0→N−W=N−0
2 zcn ⊢N∈ℤ→N∈ℂ
3 2 subid1d ⊢N∈ℤ→N−0=N
4 3 adantl ⊢W∈WordV∧N∈ℤ→N−0=N
5 1 4 sylan9eq ⊢W=0∧W∈WordV∧N∈ℤ→N−W=N
6 5 eqcomd ⊢W=0∧W∈WordV∧N∈ℤ→N=N−W
7 6 oveq2d ⊢W=0∧W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W
8 7 ex ⊢W=0→W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W
9 zre ⊢N∈ℤ→N∈ℝ
10 9 adantl ⊢W∈WordV∧N∈ℤ→N∈ℝ
11 lencl ⊢W∈WordV→W∈ℕ0
12 elnnne0 ⊢W∈ℕ↔W∈ℕ0∧W≠0
13 nnrp ⊢W∈ℕ→W∈ℝ+
14 12 13 sylbir ⊢W∈ℕ0∧W≠0→W∈ℝ+
15 14 ex ⊢W∈ℕ0→W≠0→W∈ℝ+
16 11 15 syl ⊢W∈WordV→W≠0→W∈ℝ+
17 16 adantr ⊢W∈WordV∧N∈ℤ→W≠0→W∈ℝ+
18 17 impcom ⊢W≠0∧W∈WordV∧N∈ℤ→W∈ℝ+
19 modeqmodmin ⊢N∈ℝ∧W∈ℝ+→NmodW=N−WmodW
20 10 18 19 syl2an2 ⊢W≠0∧W∈WordV∧N∈ℤ→NmodW=N−WmodW
21 20 oveq2d ⊢W≠0∧W∈WordV∧N∈ℤ→WcyclShiftNmodW=WcyclShiftN−WmodW
22 cshwmodn ⊢W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftNmodW
23 22 adantl ⊢W≠0∧W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftNmodW
24 simpl ⊢W∈WordV∧N∈ℤ→W∈WordV
25 11 nn0zd ⊢W∈WordV→W∈ℤ
26 zsubcl ⊢N∈ℤ∧W∈ℤ→N−W∈ℤ
27 25 26 sylan2 ⊢N∈ℤ∧W∈WordV→N−W∈ℤ
28 27 ancoms ⊢W∈WordV∧N∈ℤ→N−W∈ℤ
29 24 28 jca ⊢W∈WordV∧N∈ℤ→W∈WordV∧N−W∈ℤ
30 29 adantl ⊢W≠0∧W∈WordV∧N∈ℤ→W∈WordV∧N−W∈ℤ
31 cshwmodn ⊢W∈WordV∧N−W∈ℤ→WcyclShiftN−W=WcyclShiftN−WmodW
32 30 31 syl ⊢W≠0∧W∈WordV∧N∈ℤ→WcyclShiftN−W=WcyclShiftN−WmodW
33 21 23 32 3eqtr4d ⊢W≠0∧W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W
34 33 ex ⊢W≠0→W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W
35 8 34 pm2.61ine ⊢W∈WordV∧N∈ℤ→WcyclShiftN=WcyclShiftN−W