Metamath Proof Explorer

Theorem cshwidx0

Description: The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion cshwidx0 ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N

Proof

Step Hyp Ref Expression
1 hasheq0 ⊢ W ∈ Word V → W = 0 ↔ W = ∅
2 elfzo0 ⊢ N ∈ 0 ..^ W ↔ N ∈ ℕ 0 ∧ W ∈ ℕ ∧ N < W
3 elnnne0 ⊢ W ∈ ℕ ↔ W ∈ ℕ 0 ∧ W ≠ 0
4 eqneqall ⊢ W = 0 → W ≠ 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
5 4 com12 ⊢ W ≠ 0 → W = 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
6 5 adantl ⊢ W ∈ ℕ 0 ∧ W ≠ 0 → W = 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
7 3 6 sylbi ⊢ W ∈ ℕ → W = 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
8 7 3ad2ant2 ⊢ N ∈ ℕ 0 ∧ W ∈ ℕ ∧ N < W → W = 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
9 2 8 sylbi ⊢ N ∈ 0 ..^ W → W = 0 → W ∈ Word V → W cyclShift N ⁡ 0 = W ⁡ N
10 9 com13 ⊢ W ∈ Word V → W = 0 → N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N
11 1 10 sylbird ⊢ W ∈ Word V → W = ∅ → N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N
12 11 com23 ⊢ W ∈ Word V → N ∈ 0 ..^ W → W = ∅ → W cyclShift N ⁡ 0 = W ⁡ N
13 12 imp ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W = ∅ → W cyclShift N ⁡ 0 = W ⁡ N
14 13 com12 ⊢ W = ∅ → W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N
15 simpl ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W ∈ Word V
16 15 adantl ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → W ∈ Word V
17 simpl ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → W ≠ ∅
18 elfzoelz ⊢ N ∈ 0 ..^ W → N ∈ ℤ
19 18 ad2antll ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → N ∈ ℤ
20 cshwidx0mod ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ N ∈ ℤ → W cyclShift N ⁡ 0 = W ⁡ N mod W
21 16 17 19 20 syl3anc ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N mod W
22 zmodidfzoimp ⊢ N ∈ 0 ..^ W → N mod W = N
23 22 ad2antll ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → N mod W = N
24 23 fveq2d ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → W ⁡ N mod W = W ⁡ N
25 21 24 eqtrd ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N
26 25 ex ⊢ W ≠ ∅ → W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N
27 14 26 pm2.61ine ⊢ W ∈ Word V ∧ N ∈ 0 ..^ W → W cyclShift N ⁡ 0 = W ⁡ N