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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )

Proof

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