Metamath Proof Explorer

Theorem cshwrnid

Description: Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Assertion cshwrnid ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 )

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑖 ∈ ℤ )
2 1 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ℤ )
3 simp2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
4 2 3 zsubcld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑖 − 𝑁 ) ∈ ℤ )
5 elfzo0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝑊 ) ) )
6 5 simp2bi ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
7 6 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
8 zmodfzo ⊢ ( ( ( 𝑖 − 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
9 4 7 8 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
10 9 3expa ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑗 ∈ ℤ )
12 11 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑗 ∈ ℤ )
13 simplr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
14 12 13 zaddcld ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑗 + 𝑁 ) ∈ ℤ )
15 elfzo0 ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑗 < ( ♯ ‘ 𝑊 ) ) )
16 15 simp2bi ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
17 16 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
18 zmodfzo ⊢ ( ( ( 𝑗 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
19 14 17 18 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 simpr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 = ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → 𝑖 = ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
21 20 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 = ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑖 − 𝑁 ) = ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) )
22 21 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 = ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
23 22 eqeq2d ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 = ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ↔ 𝑗 = ( ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
24 12 zred ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑗 ∈ ℝ )
25 13 zred ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℝ )
26 24 25 readdcld ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑗 + 𝑁 ) ∈ ℝ )
27 17 nnrpd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
28 modsubmod ⊢ ( ( ( 𝑗 + 𝑁 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝑗 + 𝑁 ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
29 26 25 27 28 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝑗 + 𝑁 ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
30 12 zcnd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑗 ∈ ℂ )
31 13 zcnd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℂ )
32 30 31 pncand ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑗 + 𝑁 ) − 𝑁 ) = 𝑗 )
33 32 oveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑗 + 𝑁 ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑗 mod ( ♯ ‘ 𝑊 ) ) )
34 zmodidfzoimp ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑗 mod ( ♯ ‘ 𝑊 ) ) = 𝑗 )
35 34 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑗 mod ( ♯ ‘ 𝑊 ) ) = 𝑗 )
36 29 33 35 3eqtrrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑗 = ( ( ( ( 𝑗 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
37 19 23 36 rspcedvd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
38 simp3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
39 38 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) = ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
40 simp1l ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
41 simp1r ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
42 simp2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
43 cshwidxmodr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝑖 ) )
44 40 41 42 43 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 𝑖 ) )
45 39 44 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) = ( 𝑊 ‘ 𝑖 ) )
46 45 eqeq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑗 = ( ( 𝑖 − 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑐 = ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) ↔ 𝑐 = ( 𝑊 ‘ 𝑖 ) ) )
47 10 37 46 rexxfrd2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( 𝑊 ‘ 𝑖 ) ) )
48 47 abbidv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → { 𝑐 ∣ ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) } = { 𝑐 ∣ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( 𝑊 ‘ 𝑖 ) } )
49 cshwfn ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
50 fnrnfv ⊢ ( ( 𝑊 cyclShift 𝑁 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ran ( 𝑊 cyclShift 𝑁 ) = { 𝑐 ∣ ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) } )
51 49 50 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) = { 𝑐 ∣ ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝑗 ) } )
52 wrdfn ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
53 52 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
54 fnrnfv ⊢ ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ran 𝑊 = { 𝑐 ∣ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( 𝑊 ‘ 𝑖 ) } )
55 53 54 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran 𝑊 = { 𝑐 ∣ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑐 = ( 𝑊 ‘ 𝑖 ) } )
56 48 51 55 3eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 )