Metamath Proof Explorer

Theorem cshwrnid

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

Ref Expression
Assertion cshwrnid ⊢W∈WordV∧N∈ℤ→ran⁡WcyclShiftN=ran⁡W

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢i∈0..^W→i∈ℤ
2 1 3ad2ant3 ⊢W∈WordV∧N∈ℤ∧i∈0..^W→i∈ℤ
3 simp2 ⊢W∈WordV∧N∈ℤ∧i∈0..^W→N∈ℤ
4 2 3 zsubcld ⊢W∈WordV∧N∈ℤ∧i∈0..^W→i−N∈ℤ
5 elfzo0 ⊢i∈0..^W↔i∈ℕ0∧W∈ℕ∧i<W
6 5 simp2bi ⊢i∈0..^W→W∈ℕ
7 6 3ad2ant3 ⊢W∈WordV∧N∈ℤ∧i∈0..^W→W∈ℕ
8 zmodfzo ⊢i−N∈ℤ∧W∈ℕ→i−NmodW∈0..^W
9 4 7 8 syl2anc ⊢W∈WordV∧N∈ℤ∧i∈0..^W→i−NmodW∈0..^W
10 9 3expa ⊢W∈WordV∧N∈ℤ∧i∈0..^W→i−NmodW∈0..^W
11 elfzoelz ⊢j∈0..^W→j∈ℤ
12 11 adantl ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j∈ℤ
13 simplr ⊢W∈WordV∧N∈ℤ∧j∈0..^W→N∈ℤ
14 12 13 zaddcld ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+N∈ℤ
15 elfzo0 ⊢j∈0..^W↔j∈ℕ0∧W∈ℕ∧j<W
16 15 simp2bi ⊢j∈0..^W→W∈ℕ
17 16 adantl ⊢W∈WordV∧N∈ℤ∧j∈0..^W→W∈ℕ
18 zmodfzo ⊢j+N∈ℤ∧W∈ℕ→j+NmodW∈0..^W
19 14 17 18 syl2anc ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+NmodW∈0..^W
20 simpr ⊢W∈WordV∧N∈ℤ∧j∈0..^W∧i=j+NmodW→i=j+NmodW
21 20 oveq1d ⊢W∈WordV∧N∈ℤ∧j∈0..^W∧i=j+NmodW→i−N=j+NmodW−N
22 21 oveq1d ⊢W∈WordV∧N∈ℤ∧j∈0..^W∧i=j+NmodW→i−NmodW=j+NmodW−NmodW
23 22 eqeq2d ⊢W∈WordV∧N∈ℤ∧j∈0..^W∧i=j+NmodW→j=i−NmodW↔j=j+NmodW−NmodW
24 12 zred ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j∈ℝ
25 13 zred ⊢W∈WordV∧N∈ℤ∧j∈0..^W→N∈ℝ
26 24 25 readdcld ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+N∈ℝ
27 17 nnrpd ⊢W∈WordV∧N∈ℤ∧j∈0..^W→W∈ℝ+
28 modsubmod ⊢j+N∈ℝ∧N∈ℝ∧W∈ℝ+→j+NmodW−NmodW=j+N-NmodW
29 26 25 27 28 syl3anc ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+NmodW−NmodW=j+N-NmodW
30 12 zcnd ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j∈ℂ
31 13 zcnd ⊢W∈WordV∧N∈ℤ∧j∈0..^W→N∈ℂ
32 30 31 pncand ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+N-N=j
33 32 oveq1d ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j+N-NmodW=jmodW
34 zmodidfzoimp ⊢j∈0..^W→jmodW=j
35 34 adantl ⊢W∈WordV∧N∈ℤ∧j∈0..^W→jmodW=j
36 29 33 35 3eqtrrd ⊢W∈WordV∧N∈ℤ∧j∈0..^W→j=j+NmodW−NmodW
37 19 23 36 rspcedvd ⊢W∈WordV∧N∈ℤ∧j∈0..^W→∃i∈0..^Wj=i−NmodW
38 simp3 ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→j=i−NmodW
39 38 fveq2d ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→WcyclShiftN⁡j=WcyclShiftN⁡i−NmodW
40 simp1l ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→W∈WordV
41 simp1r ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→N∈ℤ
42 simp2 ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→i∈0..^W
43 cshwidxmodr ⊢W∈WordV∧N∈ℤ∧i∈0..^W→WcyclShiftN⁡i−NmodW=W⁡i
44 40 41 42 43 syl3anc ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→WcyclShiftN⁡i−NmodW=W⁡i
45 39 44 eqtrd ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→WcyclShiftN⁡j=W⁡i
46 45 eqeq2d ⊢W∈WordV∧N∈ℤ∧i∈0..^W∧j=i−NmodW→c=WcyclShiftN⁡j↔c=W⁡i
47 10 37 46 rexxfrd2 ⊢W∈WordV∧N∈ℤ→∃j∈0..^Wc=WcyclShiftN⁡j↔∃i∈0..^Wc=W⁡i
48 47 abbidv ⊢W∈WordV∧N∈ℤ→c|∃j∈0..^Wc=WcyclShiftN⁡j=c|∃i∈0..^Wc=W⁡i
49 cshwfn ⊢W∈WordV∧N∈ℤ→WcyclShiftNFn0..^W
50 fnrnfv ⊢WcyclShiftNFn0..^W→ran⁡WcyclShiftN=c|∃j∈0..^Wc=WcyclShiftN⁡j
51 49 50 syl ⊢W∈WordV∧N∈ℤ→ran⁡WcyclShiftN=c|∃j∈0..^Wc=WcyclShiftN⁡j
52 wrdfn ⊢W∈WordV→WFn0..^W
53 52 adantr ⊢W∈WordV∧N∈ℤ→WFn0..^W
54 fnrnfv ⊢WFn0..^W→ran⁡W=c|∃i∈0..^Wc=W⁡i
55 53 54 syl ⊢W∈WordV∧N∈ℤ→ran⁡W=c|∃i∈0..^Wc=W⁡i
56 48 51 55 3eqtr4d ⊢W∈WordV∧N∈ℤ→ran⁡WcyclShiftN=ran⁡W