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 e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> N e. ZZ )
2 cshwlen 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
3 1 2 sylan2 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
4 3 oveq1d 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( # ` ( W cyclShift N ) ) - 1 ) = ( ( # ` W ) - 1 ) )
5 4 oveq2d 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) = ( 0 ..^ ( ( # ` W ) - 1 ) ) )
6 5 eleq2d 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) <-> j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) )
7 6 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) -> ( j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) <-> j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) )
8 simpll 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> W e. Word V )
9 1 ad2antlr 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> N e. ZZ )
10 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
11 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
12 peano2zm 
 |-  ( ( # ` W ) e. ZZ -> ( ( # ` W ) - 1 ) e. ZZ )
13 11 12 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) e. ZZ )
14 nn0re 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. RR )
15 14 lem1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) <_ ( # ` W ) )
16 eluz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` ( ( # ` W ) - 1 ) ) <-> ( ( ( # ` W ) - 1 ) e. ZZ /\ ( # ` W ) e. ZZ /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) )
17 13 11 15 16 syl3anbrc 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( ZZ>= ` ( ( # ` W ) - 1 ) ) )
18 10 17 syl 
 |-  ( W e. Word V -> ( # ` W ) e. ( ZZ>= ` ( ( # ` W ) - 1 ) ) )
19 18 adantr 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` W ) e. ( ZZ>= ` ( ( # ` W ) - 1 ) ) )
20 fzoss2 
 |-  ( ( # ` W ) e. ( ZZ>= ` ( ( # ` W ) - 1 ) ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( # ` W ) ) )
21 19 20 syl 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( ( # ` W ) - 1 ) ) C_ ( 0 ..^ ( # ` W ) ) )
22 21 sselda 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> j e. ( 0 ..^ ( # ` W ) ) )
23 cshwidxmod 
 |-  ( ( W e. Word V /\ N e. ZZ /\ j e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` j ) = ( W ` ( ( j + N ) mod ( # ` W ) ) ) )
24 8 9 22 23 syl3anc 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W cyclShift N ) ` j ) = ( W ` ( ( j + N ) mod ( # ` W ) ) ) )
25 elfzo1 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) <-> ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) )
26 25 simp2bi 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
27 26 adantl 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN )
28 elfzom1p1elfzo 
 |-  ( ( ( # ` W ) e. NN /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( j + 1 ) e. ( 0 ..^ ( # ` W ) ) )
29 27 28 sylan 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( j + 1 ) e. ( 0 ..^ ( # ` W ) ) )
30 cshwidxmod 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( j + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` ( j + 1 ) ) = ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) )
31 8 9 29 30 syl3anc 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W cyclShift N ) ` ( j + 1 ) ) = ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) )
32 24 31 preq12d 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } = { ( W ` ( ( j + N ) mod ( # ` W ) ) ) , ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) } )
33 32 adantlr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } = { ( W ` ( ( j + N ) mod ( # ` W ) ) ) , ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) } )
34 2z 
 |-  2 e. ZZ
35 34 a1i 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 2 e. ZZ )
36 nnz 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. ZZ )
37 36 3ad2ant2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) e. ZZ )
38 nnnn0 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. NN0 )
39 38 3ad2ant2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) e. NN0 )
40 nnne0 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) =/= 0 )
41 40 3ad2ant2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) =/= 0 )
42 1red 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 1 e. RR )
43 nnre 
 |-  ( N e. NN -> N e. RR )
44 43 3ad2ant1 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> N e. RR )
45 nnre 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR )
46 45 3ad2ant2 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) e. RR )
47 nnge1 
 |-  ( N e. NN -> 1 <_ N )
48 47 3ad2ant1 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 1 <_ N )
49 simp3 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> N < ( # ` W ) )
50 42 44 46 48 49 lelttrd 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 1 < ( # ` W ) )
51 42 50 gtned 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) =/= 1 )
52 nn0n0n1ge2 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 /\ ( # ` W ) =/= 1 ) -> 2 <_ ( # ` W ) )
53 39 41 51 52 syl3anc 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> 2 <_ ( # ` W ) )
54 eluz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` W ) e. ZZ /\ 2 <_ ( # ` W ) ) )
55 35 37 53 54 syl3anbrc 
 |-  ( ( N e. NN /\ ( # ` W ) e. NN /\ N < ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
56 25 55 sylbi 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
57 56 ad3antlr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
58 elfzoelz 
 |-  ( j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> j e. ZZ )
59 58 adantl 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> j e. ZZ )
60 1 ad3antlr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> N e. ZZ )
61 simplrl 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E )
62 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
63 62 adantr 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
64 63 preq1d 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } )
65 64 eleq1d 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. E <-> { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E ) )
66 65 biimpcd 
 |-  ( { ( lastS ` W ) , ( W ` 0 ) } e. E -> ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E ) )
67 66 adantl 
 |-  ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E ) )
68 67 impcom 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) -> { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E )
69 68 adantr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E )
70 clwwisshclwwslemlem 
 |-  ( ( ( ( # ` W ) e. ( ZZ>= ` 2 ) /\ j e. ZZ /\ N e. ZZ ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( W ` ( ( # ` W ) - 1 ) ) , ( W ` 0 ) } e. E ) -> { ( W ` ( ( j + N ) mod ( # ` W ) ) ) , ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) } e. E )
71 57 59 60 61 69 70 syl311anc 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( W ` ( ( j + N ) mod ( # ` W ) ) ) , ( W ` ( ( ( j + 1 ) + N ) mod ( # ` W ) ) ) } e. E )
72 33 71 eqeltrd 
 |-  ( ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) /\ j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E )
73 72 ex 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) -> ( j e. ( 0 ..^ ( ( # ` W ) - 1 ) ) -> { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E ) )
74 7 73 sylbid 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) -> ( j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) -> { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E ) )
75 74 ralrimiv 
 |-  ( ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) ) -> A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E )
76 75 ex 
 |-  ( ( W e. Word V /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. E ) )