Metamath Proof Explorer

Theorem clwwisshclwwslem

Description: Lemma for clwwisshclwws . (Contributed by AV, 24-Mar-2018) (Revised by AV, 28-Apr-2021)

Ref Expression
Assertion clwwisshclwwslem ⊢W∈WordV∧N∈1..^W→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→∀j∈0..^WcyclShiftN−1WcyclShiftN⁡jWcyclShiftN⁡j+1∈E

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢N∈1..^W→N∈ℤ
2 cshwlen ⊢W∈WordV∧N∈ℤ→WcyclShiftN=W
3 1 2 sylan2 ⊢W∈WordV∧N∈1..^W→WcyclShiftN=W
4 3 oveq1d ⊢W∈WordV∧N∈1..^W→WcyclShiftN−1=W−1
5 4 oveq2d ⊢W∈WordV∧N∈1..^W→0..^WcyclShiftN−1=0..^W−1
6 5 eleq2d ⊢W∈WordV∧N∈1..^W→j∈0..^WcyclShiftN−1↔j∈0..^W−1
7 6 adantr ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→j∈0..^WcyclShiftN−1↔j∈0..^W−1
8 simpll ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→W∈WordV
9 1 ad2antlr ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→N∈ℤ
10 lencl ⊢W∈WordV→W∈ℕ0
11 nn0z ⊢W∈ℕ0→W∈ℤ
12 peano2zm ⊢W∈ℤ→W−1∈ℤ
13 11 12 syl ⊢W∈ℕ0→W−1∈ℤ
14 nn0re ⊢W∈ℕ0→W∈ℝ
15 14 lem1d ⊢W∈ℕ0→W−1≤W
16 eluz2 ⊢W∈ℤ≥W−1↔W−1∈ℤ∧W∈ℤ∧W−1≤W
17 13 11 15 16 syl3anbrc ⊢W∈ℕ0→W∈ℤ≥W−1
18 10 17 syl ⊢W∈WordV→W∈ℤ≥W−1
19 18 adantr ⊢W∈WordV∧N∈1..^W→W∈ℤ≥W−1
20 fzoss2 ⊢W∈ℤ≥W−1→0..^W−1⊆0..^W
21 19 20 syl ⊢W∈WordV∧N∈1..^W→0..^W−1⊆0..^W
22 21 sselda ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→j∈0..^W
23 cshwidxmod ⊢W∈WordV∧N∈ℤ∧j∈0..^W→WcyclShiftN⁡j=W⁡j+NmodW
24 8 9 22 23 syl3anc ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→WcyclShiftN⁡j=W⁡j+NmodW
25 elfzo1 ⊢N∈1..^W↔N∈ℕ∧W∈ℕ∧N<W
26 25 simp2bi ⊢N∈1..^W→W∈ℕ
27 26 adantl ⊢W∈WordV∧N∈1..^W→W∈ℕ
28 elfzom1p1elfzo ⊢W∈ℕ∧j∈0..^W−1→j+1∈0..^W
29 27 28 sylan ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→j+1∈0..^W
30 cshwidxmod ⊢W∈WordV∧N∈ℤ∧j+1∈0..^W→WcyclShiftN⁡j+1=W⁡j+1+NmodW
31 8 9 29 30 syl3anc ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→WcyclShiftN⁡j+1=W⁡j+1+NmodW
32 24 31 preq12d ⊢W∈WordV∧N∈1..^W∧j∈0..^W−1→WcyclShiftN⁡jWcyclShiftN⁡j+1=W⁡j+NmodWW⁡j+1+NmodW
33 32 adantlr ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→WcyclShiftN⁡jWcyclShiftN⁡j+1=W⁡j+NmodWW⁡j+1+NmodW
34 2z ⊢2∈ℤ
35 34 a1i ⊢N∈ℕ∧W∈ℕ∧N<W→2∈ℤ
36 nnz ⊢W∈ℕ→W∈ℤ
37 36 3ad2ant2 ⊢N∈ℕ∧W∈ℕ∧N<W→W∈ℤ
38 nnnn0 ⊢W∈ℕ→W∈ℕ0
39 38 3ad2ant2 ⊢N∈ℕ∧W∈ℕ∧N<W→W∈ℕ0
40 nnne0 ⊢W∈ℕ→W≠0
41 40 3ad2ant2 ⊢N∈ℕ∧W∈ℕ∧N<W→W≠0
42 1red ⊢N∈ℕ∧W∈ℕ∧N<W→1∈ℝ
43 nnre ⊢N∈ℕ→N∈ℝ
44 43 3ad2ant1 ⊢N∈ℕ∧W∈ℕ∧N<W→N∈ℝ
45 nnre ⊢W∈ℕ→W∈ℝ
46 45 3ad2ant2 ⊢N∈ℕ∧W∈ℕ∧N<W→W∈ℝ
47 nnge1 ⊢N∈ℕ→1≤N
48 47 3ad2ant1 ⊢N∈ℕ∧W∈ℕ∧N<W→1≤N
49 simp3 ⊢N∈ℕ∧W∈ℕ∧N<W→N<W
50 42 44 46 48 49 lelttrd ⊢N∈ℕ∧W∈ℕ∧N<W→1<W
51 42 50 gtned ⊢N∈ℕ∧W∈ℕ∧N<W→W≠1
52 nn0n0n1ge2 ⊢W∈ℕ0∧W≠0∧W≠1→2≤W
53 39 41 51 52 syl3anc ⊢N∈ℕ∧W∈ℕ∧N<W→2≤W
54 eluz2 ⊢W∈ℤ≥2↔2∈ℤ∧W∈ℤ∧2≤W
55 35 37 53 54 syl3anbrc ⊢N∈ℕ∧W∈ℕ∧N<W→W∈ℤ≥2
56 25 55 sylbi ⊢N∈1..^W→W∈ℤ≥2
57 56 ad3antlr ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→W∈ℤ≥2
58 elfzoelz ⊢j∈0..^W−1→j∈ℤ
59 58 adantl ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→j∈ℤ
60 1 ad3antlr ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→N∈ℤ
61 simplrl ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→∀i∈0..^W−1W⁡iW⁡i+1∈E
62 lsw ⊢W∈WordV→lastS⁡W=W⁡W−1
63 62 adantr ⊢W∈WordV∧N∈1..^W→lastS⁡W=W⁡W−1
64 63 preq1d ⊢W∈WordV∧N∈1..^W→lastS⁡WW⁡0=W⁡W−1W⁡0
65 64 eleq1d ⊢W∈WordV∧N∈1..^W→lastS⁡WW⁡0∈E↔W⁡W−1W⁡0∈E
66 65 biimpcd ⊢lastS⁡WW⁡0∈E→W∈WordV∧N∈1..^W→W⁡W−1W⁡0∈E
67 66 adantl ⊢∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→W∈WordV∧N∈1..^W→W⁡W−1W⁡0∈E
68 67 impcom ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→W⁡W−1W⁡0∈E
69 68 adantr ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→W⁡W−1W⁡0∈E
70 clwwisshclwwslemlem ⊢W∈ℤ≥2∧j∈ℤ∧N∈ℤ∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧W⁡W−1W⁡0∈E→W⁡j+NmodWW⁡j+1+NmodW∈E
71 57 59 60 61 69 70 syl311anc ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→W⁡j+NmodWW⁡j+1+NmodW∈E
72 33 71 eqeltrd ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧j∈0..^W−1→WcyclShiftN⁡jWcyclShiftN⁡j+1∈E
73 72 ex ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→j∈0..^W−1→WcyclShiftN⁡jWcyclShiftN⁡j+1∈E
74 7 73 sylbid ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→j∈0..^WcyclShiftN−1→WcyclShiftN⁡jWcyclShiftN⁡j+1∈E
75 74 ralrimiv ⊢W∈WordV∧N∈1..^W∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→∀j∈0..^WcyclShiftN−1WcyclShiftN⁡jWcyclShiftN⁡j+1∈E
76 75 ex ⊢W∈WordV∧N∈1..^W→∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→∀j∈0..^WcyclShiftN−1WcyclShiftN⁡jWcyclShiftN⁡j+1∈E