Metamath Proof Explorer

Theorem cshwn

Description: A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshwn ⊢ W ∈ Word V → W cyclShift W = W

Proof

Step Hyp Ref Expression
1 0csh0 ⊢ ∅ cyclShift W = ∅
2 oveq1 ⊢ ∅ = W → ∅ cyclShift W = W cyclShift W
3 id ⊢ ∅ = W → ∅ = W
4 1 2 3 3eqtr3a ⊢ ∅ = W → W cyclShift W = W
5 4 a1d ⊢ ∅ = W → W ∈ Word V → W cyclShift W = W
6 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
7 6 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
8 cshwmodn ⊢ W ∈ Word V ∧ W ∈ ℤ → W cyclShift W = W cyclShift W mod W
9 7 8 mpdan ⊢ W ∈ Word V → W cyclShift W = W cyclShift W mod W
10 9 adantl ⊢ ∅ ≠ W ∧ W ∈ Word V → W cyclShift W = W cyclShift W mod W
11 necom ⊢ ∅ ≠ W ↔ W ≠ ∅
12 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
13 11 12 sylan2b ⊢ W ∈ Word V ∧ ∅ ≠ W → W ∈ ℕ
14 13 nnrpd ⊢ W ∈ Word V ∧ ∅ ≠ W → W ∈ ℝ +
15 14 ancoms ⊢ ∅ ≠ W ∧ W ∈ Word V → W ∈ ℝ +
16 modid0 ⊢ W ∈ ℝ + → W mod W = 0
17 15 16 syl ⊢ ∅ ≠ W ∧ W ∈ Word V → W mod W = 0
18 17 oveq2d ⊢ ∅ ≠ W ∧ W ∈ Word V → W cyclShift W mod W = W cyclShift 0
19 cshw0 ⊢ W ∈ Word V → W cyclShift 0 = W
20 19 adantl ⊢ ∅ ≠ W ∧ W ∈ Word V → W cyclShift 0 = W
21 10 18 20 3eqtrd ⊢ ∅ ≠ W ∧ W ∈ Word V → W cyclShift W = W
22 21 ex ⊢ ∅ ≠ W → W ∈ Word V → W cyclShift W = W
23 5 22 pm2.61ine ⊢ W ∈ Word V → W cyclShift W = W