Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cshweqrep Structured version   Unicode version

Theorem cshweqrep 12910
 Description: If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
Assertion
Ref Expression
cshweqrep Word cyclShift ..^
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cshweqrep
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6308 . . . . . . . . . 10
21oveq2d 6317 . . . . . . . . 9
32oveq1d 6316 . . . . . . . 8
43fveq2d 5881 . . . . . . 7
54eqeq2d 2436 . . . . . 6
65imbi2d 317 . . . . 5 Word cyclShift ..^ Word cyclShift ..^
7 oveq1 6308 . . . . . . . . . 10
87oveq2d 6317 . . . . . . . . 9
98oveq1d 6316 . . . . . . . 8
109fveq2d 5881 . . . . . . 7
1110eqeq2d 2436 . . . . . 6
1211imbi2d 317 . . . . 5 Word cyclShift ..^ Word cyclShift ..^
13 oveq1 6308 . . . . . . . . . 10
1413oveq2d 6317 . . . . . . . . 9
1514oveq1d 6316 . . . . . . . 8
1615fveq2d 5881 . . . . . . 7
1716eqeq2d 2436 . . . . . 6
1817imbi2d 317 . . . . 5 Word cyclShift ..^ Word cyclShift ..^
19 oveq1 6308 . . . . . . . . . 10
2019oveq2d 6317 . . . . . . . . 9
2120oveq1d 6316 . . . . . . . 8
2221fveq2d 5881 . . . . . . 7
2322eqeq2d 2436 . . . . . 6
2423imbi2d 317 . . . . 5 Word cyclShift ..^ Word cyclShift ..^
25 zcn 10942 . . . . . . . . . . . . 13
2625mul02d 9831 . . . . . . . . . . . 12
2726adantl 467 . . . . . . . . . . 11 Word
2827adantr 466 . . . . . . . . . 10 Word cyclShift ..^
2928oveq2d 6317 . . . . . . . . 9 Word cyclShift ..^
30 elfzoelz 11920 . . . . . . . . . . . 12 ..^
3130zcnd 11041 . . . . . . . . . . 11 ..^
3231addid1d 9833 . . . . . . . . . 10 ..^
3332ad2antll 733 . . . . . . . . 9 Word cyclShift ..^
3429, 33eqtrd 2463 . . . . . . . 8 Word cyclShift ..^
3534oveq1d 6316 . . . . . . 7 Word cyclShift ..^
36 zmodidfzoimp 12126 . . . . . . . 8 ..^
3736ad2antll 733 . . . . . . 7 Word cyclShift ..^
3835, 37eqtr2d 2464 . . . . . 6 Word cyclShift ..^
3938fveq2d 5881 . . . . 5 Word cyclShift ..^
40 fveq1 5876 . . . . . . . . . . . . 13 cyclShift cyclShift
4140eqcoms 2434 . . . . . . . . . . . 12 cyclShift cyclShift
4241ad2antrl 732 . . . . . . . . . . 11 Word cyclShift ..^ cyclShift
4342adantl 467 . . . . . . . . . 10 Word cyclShift ..^ cyclShift
44 simprll 770 . . . . . . . . . . 11 Word cyclShift ..^ Word
45 simprlr 771 . . . . . . . . . . 11 Word cyclShift ..^
46 elfzo0 11956 . . . . . . . . . . . . . . . . . . 19 ..^
47 nn0z 10960 . . . . . . . . . . . . . . . . . . . . . . . 24
4847adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23
49 nn0z 10960 . . . . . . . . . . . . . . . . . . . . . . . . 25
50 zmulcl 10985 . . . . . . . . . . . . . . . . . . . . . . . . 25
5149, 50sylan 473 . . . . . . . . . . . . . . . . . . . . . . . 24
5251ancoms 454 . . . . . . . . . . . . . . . . . . . . . . 23
53 zaddcl 10977 . . . . . . . . . . . . . . . . . . . . . . 23
5448, 52, 53syl2an 479 . . . . . . . . . . . . . . . . . . . . . 22
55 simplr 760 . . . . . . . . . . . . . . . . . . . . . 22
5654, 55jca 534 . . . . . . . . . . . . . . . . . . . . 21
5756ex 435 . . . . . . . . . . . . . . . . . . . 20
58573adant3 1025 . . . . . . . . . . . . . . . . . . 19
5946, 58sylbi 198 . . . . . . . . . . . . . . . . . 18 ..^
6059adantl 467 . . . . . . . . . . . . . . . . 17 cyclShift ..^
6160expd 437 . . . . . . . . . . . . . . . 16 cyclShift ..^
6261com12 32 . . . . . . . . . . . . . . 15 cyclShift ..^
6362adantl 467 . . . . . . . . . . . . . 14 Word cyclShift ..^
6463imp 430 . . . . . . . . . . . . 13 Word cyclShift ..^
6564impcom 431 . . . . . . . . . . . 12 Word cyclShift ..^
66 zmodfzo 12118 . . . . . . . . . . . 12 ..^
6765, 66syl 17 . . . . . . . . . . 11 Word cyclShift ..^ ..^
68 cshwidxmod 12895 . . . . . . . . . . 11 Word ..^ cyclShift
6944, 45, 67, 68syl3anc 1264 . . . . . . . . . 10 Word cyclShift ..^ cyclShift
70 nn0re 10878 . . . . . . . . . . . . . . . . . . . 20
71 zre 10941 . . . . . . . . . . . . . . . . . . . . . 22
72 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . 22
73 nnrp 11311 . . . . . . . . . . . . . . . . . . . . . . . . 25
74 remulcl 9624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7574ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
76 readdcl 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7775, 76sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7877ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7978adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80 simprll 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
82 modaddmod 12135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8379, 80, 81, 82syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
84 recn 9629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8584adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8674recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8786ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8887adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
89 recn 9629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9089adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9190adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9285, 88, 91addassd 9665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
93 recn 9629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9493adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
95 1cnd 9659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9694, 95, 90adddird 9668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9789mulid2d 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9897adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9998oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
10096, 99eqtr2d 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101100adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102101oveq2d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10392, 102eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104103adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105104oveq1d 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10683, 105eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
107106ex 435 . . . . . . . . . . . . . . . . . . . . . . . . 25
10873, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
109108expd 437 . . . . . . . . . . . . . . . . . . . . . . 23
110109com12 32 . . . . . . . . . . . . . . . . . . . . . 22
11171, 72, 110syl2an 479 . . . . . . . . . . . . . . . . . . . . 21
112111com13 83 . . . . . . . . . . . . . . . . . . . 20
11370, 112syl 17 . . . . . . . . . . . . . . . . . . 19
114113imp 430 . . . . . . . . . . . . . . . . . 18
1151143adant3 1025 . . . . . . . . . . . . . . . . 17
11646, 115sylbi 198 . . . . . . . . . . . . . . . 16 ..^
117116expd 437 . . . . . . . . . . . . . . 15 ..^
118117adantld 468 . . . . . . . . . . . . . 14 ..^ Word
119118adantl 467 . . . . . . . . . . . . 13 cyclShift ..^ Word
120119impcom 431 . . . . . . . . . . . 12 Word cyclShift ..^
121120impcom 431 . . . . . . . . . . 11 Word cyclShift ..^
122121fveq2d 5881 . . . . . . . . . 10 Word cyclShift ..^
12343, 69, 1223eqtrd 2467 . . . . . . . . 9 Word cyclShift ..^
124123eqeq2d 2436 . . . . . . . 8 Word cyclShift ..^
125124biimpd 210 . . . . . . 7 Word cyclShift ..^
126125ex 435 . . . . . 6 Word cyclShift ..^
127126a2d 29 . . . . 5 Word cyclShift ..^ Word cyclShift ..^
1286, 12, 18, 24, 39, 127nn0ind 11030 . . . 4 Word cyclShift ..^
129128com12 32 . . 3 Word cyclShift ..^
130129ralrimiv 2837 . 2 Word cyclShift ..^
131130ex 435 1 Word cyclShift ..^
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868  wral 2775   class class class wbr 4420  cfv 5597  (class class class)co 6301  cc 9537  cr 9538  cc0 9539  c1 9540   caddc 9542   cmul 9544   clt 9675  cn 10609  cn0 10869  cz 10937  crp 11302  ..^cfzo 11915   cmo 12095  chash 12514  Word cword 12648   cyclShift ccsh 12880 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-oadd 7190  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-sup 7958  df-inf 7959  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-fz 11785  df-fzo 11916  df-fl 12027  df-mod 12096  df-hash 12515  df-word 12656  df-concat 12658  df-substr 12660  df-csh 12881 This theorem is referenced by:  cshw1  12911  cshwsidrepsw  15051
 Copyright terms: Public domain W3C validator