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 ( 𝑁 − ( ♯ ‘ 𝑊 ) ) ) )