Metamath Proof Explorer

Theorem cshwlen

Description: The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 27-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

Ref Expression
Assertion cshwlen ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W

Proof

Step Hyp Ref Expression
1 0csh0 ⊢ ∅ cyclShift N = ∅
2 oveq1 ⊢ W = ∅ → W cyclShift N = ∅ cyclShift N
3 id ⊢ W = ∅ → W = ∅
4 1 2 3 3eqtr4a ⊢ W = ∅ → W cyclShift N = W
5 4 fveq2d ⊢ W = ∅ → W cyclShift N = W
6 5 a1d ⊢ W = ∅ → W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W
7 cshword ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W substr N mod W W ++ W prefix N mod W
8 7 fveq2d ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W substr N mod W W ++ W prefix N mod W
9 8 adantr ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W ≠ ∅ → W cyclShift N = W substr N mod W W ++ W prefix N mod W
10 swrdcl ⊢ W ∈ Word V → W substr N mod W W ∈ Word V
11 pfxcl ⊢ W ∈ Word V → W prefix N mod W ∈ Word V
12 ccatlen ⊢ 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 = W substr N mod W W + W prefix N mod W
13 10 11 12 syl2anc ⊢ W ∈ Word V → W substr N mod W W ++ W prefix N mod W = W substr N mod W W + W prefix N mod W
14 13 ad2antrr ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W ≠ ∅ → W substr N mod W W ++ W prefix N mod W = W substr N mod W W + W prefix N mod W
15 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
16 pm3.21 ⊢ W ∈ ℕ ∧ N ∈ ℤ → W ∈ Word V → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
17 16 ex ⊢ W ∈ ℕ → N ∈ ℤ → W ∈ Word V → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
18 15 17 syl ⊢ W ∈ Word V ∧ W ≠ ∅ → N ∈ ℤ → W ∈ Word V → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
19 18 ex ⊢ W ∈ Word V → W ≠ ∅ → N ∈ ℤ → W ∈ Word V → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
20 19 com24 ⊢ W ∈ Word V → W ∈ Word V → N ∈ ℤ → W ≠ ∅ → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
21 20 pm2.43i ⊢ W ∈ Word V → N ∈ ℤ → W ≠ ∅ → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
22 21 imp31 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W ≠ ∅ → W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ
23 simpl ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W ∈ Word V
24 zmodfzp1 ⊢ N ∈ ℤ ∧ W ∈ ℕ → N mod W ∈ 0 … W
25 24 ancoms ⊢ W ∈ ℕ ∧ N ∈ ℤ → N mod W ∈ 0 … W
26 25 adantl ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → N mod W ∈ 0 … W
27 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
28 nn0fz0 ⊢ W ∈ ℕ 0 ↔ W ∈ 0 … W
29 27 28 sylib ⊢ W ∈ Word V → W ∈ 0 … W
30 29 adantr ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W ∈ 0 … W
31 swrdlen ⊢ W ∈ Word V ∧ N mod W ∈ 0 … W ∧ W ∈ 0 … W → W substr N mod W W = W − N mod W
32 23 26 30 31 syl3anc ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W substr N mod W W = W − N mod W
33 pfxlen ⊢ W ∈ Word V ∧ N mod W ∈ 0 … W → W prefix N mod W = N mod W
34 25 33 sylan2 ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W prefix N mod W = N mod W
35 32 34 oveq12d ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W substr N mod W W + W prefix N mod W = W - N mod W + N mod W
36 27 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
37 zmodcl ⊢ N ∈ ℤ ∧ W ∈ ℕ → N mod W ∈ ℕ 0
38 37 nn0cnd ⊢ N ∈ ℤ ∧ W ∈ ℕ → N mod W ∈ ℂ
39 38 ancoms ⊢ W ∈ ℕ ∧ N ∈ ℤ → N mod W ∈ ℂ
40 npcan ⊢ W ∈ ℂ ∧ N mod W ∈ ℂ → W - N mod W + N mod W = W
41 36 39 40 syl2an ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W - N mod W + N mod W = W
42 35 41 eqtrd ⊢ W ∈ Word V ∧ W ∈ ℕ ∧ N ∈ ℤ → W substr N mod W W + W prefix N mod W = W
43 22 42 syl ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W ≠ ∅ → W substr N mod W W + W prefix N mod W = W
44 9 14 43 3eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W ≠ ∅ → W cyclShift N = W
45 44 expcom ⊢ W ≠ ∅ → W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W
46 6 45 pm2.61ine ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W