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∈WordV∧N∈0..^W→WcyclShiftN⁡0=W⁡N

Proof

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