Metamath Proof Explorer

Theorem cshwcl

Description: A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 27-Oct-2018)

Ref Expression
Assertion cshwcl ⊢ W ∈ Word V → W cyclShift N ∈ Word V

Proof

Step Hyp Ref Expression
1 cshword ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W substr N mod W W ++ W prefix N mod W
2 swrdcl ⊢ W ∈ Word V → W substr N mod W W ∈ Word V
3 pfxcl ⊢ W ∈ Word V → W prefix N mod W ∈ Word V
4 ccatcl ⊢ W substr N mod W W ∈ Word V ∧ W prefix N mod W ∈ Word V → W substr N mod W W ++ W prefix N mod W ∈ Word V
5 2 3 4 syl2anc ⊢ W ∈ Word V → W substr N mod W W ++ W prefix N mod W ∈ Word V
6 5 adantr ⊢ W ∈ Word V ∧ N ∈ ℤ → W substr N mod W W ++ W prefix N mod W ∈ Word V
7 1 6 eqeltrd ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N ∈ Word V
8 7 expcom ⊢ N ∈ ℤ → W ∈ Word V → W cyclShift N ∈ Word V
9 cshnz ⊢ ¬ N ∈ ℤ → W cyclShift N = ∅
10 wrd0 ⊢ ∅ ∈ Word V
11 9 10 eqeltrdi ⊢ ¬ N ∈ ℤ → W cyclShift N ∈ Word V
12 11 a1d ⊢ ¬ N ∈ ℤ → W ∈ Word V → W cyclShift N ∈ Word V
13 8 12 pm2.61i ⊢ W ∈ Word V → W cyclShift N ∈ Word V