# Metamath Proof Explorer

## Theorem cshwsublen

Description: Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion cshwsublen ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) )

### Proof

Step Hyp Ref Expression
1 oveq2 ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑁 − ( ♯ ‘ 𝑊 ) ) = ( 𝑁 − 0 ) )
2 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3 2 subid1d ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 )
4 3 adantl ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑁 − 0 ) = 𝑁 )
5 1 4 sylan9eq ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑁 − ( ♯ ‘ 𝑊 ) ) = 𝑁 )
6 5 eqcomd ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → 𝑁 = ( 𝑁 − ( ♯ ‘ 𝑊 ) ) )
7 6 oveq2d ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) )
8 7 ex ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) ) )
9 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
10 9 adantl ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
11 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
12 elnnne0 ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) )
13 nnrp ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
14 12 13 sylbir ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
15 14 ex ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
16 11 15 syl ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
17 16 adantr ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) )
18 17 impcom ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
19 modeqmodmin ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑁 − ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) )
20 10 18 19 syl2an2 ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑁 − ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) )
21 20 oveq2d ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 cyclShift ( ( 𝑁 − ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
22 cshwmodn ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
23 22 adantl ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
24 simpl ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → 𝑊 ∈ Word 𝑉 )
25 11 nn0zd ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
26 zsubcl ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ) → ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
27 25 26 sylan2 ( ( 𝑁 ∈ ℤ ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
28 27 ancoms ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
29 24 28 jca ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ ) )
30 29 adantl ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ ) )
31 cshwmodn ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ∈ ℤ ) → ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 cyclShift ( ( 𝑁 − ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
32 30 31 syl ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 cyclShift ( ( 𝑁 − ( ♯ ‘ 𝑊 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
33 21 23 32 3eqtr4d ( ( ( ♯ ‘ 𝑊 ) ≠ 0 ∧ ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) )
34 33 ex ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) ) )
35 8 34 pm2.61ine ( ( 𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) )