Step | Hyp | Ref
| Expression |
1 | | cshwrepswhash1.m |
. . . . . 6
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} |
2 | 1 | cshwsiun 16980 |
. . . . 5
โข (๐ โ Word ๐ โ ๐ = โช ๐ โ
(0..^(โฏโ๐)){(๐ cyclShift ๐)}) |
3 | 2 | ad2antrr 725 |
. . . 4
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ๐ = โช ๐ โ
(0..^(โฏโ๐)){(๐ cyclShift ๐)}) |
4 | 3 | fveq2d 6850 |
. . 3
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ (โฏโ๐) = (โฏโโช ๐ โ (0..^(โฏโ๐)){(๐ cyclShift ๐)})) |
5 | | fzofi 13888 |
. . . . 5
โข
(0..^(โฏโ๐)) โ Fin |
6 | 5 | a1i 11 |
. . . 4
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ (0..^(โฏโ๐)) โ Fin) |
7 | | snfi 8994 |
. . . . 5
โข {(๐ cyclShift ๐)} โ Fin |
8 | 7 | a1i 11 |
. . . 4
โข ((((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โง ๐ โ (0..^(โฏโ๐))) โ {(๐ cyclShift ๐)} โ Fin) |
9 | | id 22 |
. . . . 5
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ (๐ โ Word ๐ โง (โฏโ๐) โ โ)) |
10 | 9 | cshwsdisj 16979 |
. . . 4
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ Disj ๐ โ
(0..^(โฏโ๐)){(๐ cyclShift ๐)}) |
11 | 6, 8, 10 | hashiun 15715 |
. . 3
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ (โฏโโช ๐ โ (0..^(โฏโ๐)){(๐ cyclShift ๐)}) = ฮฃ๐ โ (0..^(โฏโ๐))(โฏโ{(๐ cyclShift ๐)})) |
12 | | ovex 7394 |
. . . . . 6
โข (๐ cyclShift ๐) โ V |
13 | | hashsng 14278 |
. . . . . 6
โข ((๐ cyclShift ๐) โ V โ (โฏโ{(๐ cyclShift ๐)}) = 1) |
14 | 12, 13 | mp1i 13 |
. . . . 5
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ (โฏโ{(๐ cyclShift ๐)}) = 1) |
15 | 14 | sumeq2sdv 15597 |
. . . 4
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ฮฃ๐ โ (0..^(โฏโ๐))(โฏโ{(๐ cyclShift ๐)}) = ฮฃ๐ โ (0..^(โฏโ๐))1) |
16 | | 1cnd 11158 |
. . . . . . 7
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ 1 โ
โ) |
17 | | fsumconst 15683 |
. . . . . . 7
โข
(((0..^(โฏโ๐)) โ Fin โง 1 โ โ) โ
ฮฃ๐ โ
(0..^(โฏโ๐))1 =
((โฏโ(0..^(โฏโ๐))) ยท 1)) |
18 | 5, 16, 17 | sylancr 588 |
. . . . . 6
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ฮฃ๐ โ
(0..^(โฏโ๐))1 =
((โฏโ(0..^(โฏโ๐))) ยท 1)) |
19 | | lencl 14430 |
. . . . . . . . 9
โข (๐ โ Word ๐ โ (โฏโ๐) โ
โ0) |
20 | 19 | adantr 482 |
. . . . . . . 8
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
(โฏโ๐) โ
โ0) |
21 | | hashfzo0 14339 |
. . . . . . . 8
โข
((โฏโ๐)
โ โ0 โ (โฏโ(0..^(โฏโ๐))) = (โฏโ๐)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
(โฏโ(0..^(โฏโ๐))) = (โฏโ๐)) |
23 | 22 | oveq1d 7376 |
. . . . . 6
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
((โฏโ(0..^(โฏโ๐))) ยท 1) = ((โฏโ๐) ยท 1)) |
24 | | prmnn 16558 |
. . . . . . . . 9
โข
((โฏโ๐)
โ โ โ (โฏโ๐) โ โ) |
25 | 24 | nnred 12176 |
. . . . . . . 8
โข
((โฏโ๐)
โ โ โ (โฏโ๐) โ โ) |
26 | 25 | adantl 483 |
. . . . . . 7
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
(โฏโ๐) โ
โ) |
27 | | ax-1rid 11129 |
. . . . . . 7
โข
((โฏโ๐)
โ โ โ ((โฏโ๐) ยท 1) = (โฏโ๐)) |
28 | 26, 27 | syl 17 |
. . . . . 6
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ
((โฏโ๐) ยท
1) = (โฏโ๐)) |
29 | 18, 23, 28 | 3eqtrd 2777 |
. . . . 5
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ฮฃ๐ โ
(0..^(โฏโ๐))1 =
(โฏโ๐)) |
30 | 29 | adantr 482 |
. . . 4
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ฮฃ๐ โ (0..^(โฏโ๐))1 = (โฏโ๐)) |
31 | 15, 30 | eqtrd 2773 |
. . 3
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ฮฃ๐ โ (0..^(โฏโ๐))(โฏโ{(๐ cyclShift ๐)}) = (โฏโ๐)) |
32 | 4, 11, 31 | 3eqtrd 2777 |
. 2
โข (((๐ โ Word ๐ โง (โฏโ๐) โ โ) โง โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ (โฏโ๐) = (โฏโ๐)) |
33 | 32 | ex 414 |
1
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ (โ๐ โ
(0..^(โฏโ๐))(๐โ๐) โ (๐โ0) โ (โฏโ๐) = (โฏโ๐))) |