Step | Hyp | Ref
| Expression |
1 | | tocycval.1 |
. . 3
β’ πΆ = (toCycβπ·) |
2 | | tocycfv.d |
. . 3
β’ (π β π· β π) |
3 | | tocycfv.w |
. . 3
β’ (π β π β Word π·) |
4 | | tocycfv.1 |
. . 3
β’ (π β π:dom πβ1-1βπ·) |
5 | | cycpmfv2.2 |
. . . 4
β’ (π β π = ((β―βπ) β 1)) |
6 | | lencl 14427 |
. . . . . . . 8
β’ (π β Word π· β (β―βπ) β
β0) |
7 | 3, 6 | syl 17 |
. . . . . . 7
β’ (π β (β―βπ) β
β0) |
8 | | cycpmfv2.1 |
. . . . . . 7
β’ (π β 0 <
(β―βπ)) |
9 | | elnnnn0b 12462 |
. . . . . . 7
β’
((β―βπ)
β β β ((β―βπ) β β0 β§ 0 <
(β―βπ))) |
10 | 7, 8, 9 | sylanbrc 584 |
. . . . . 6
β’ (π β (β―βπ) β
β) |
11 | | elfz1end 13477 |
. . . . . 6
β’
((β―βπ)
β β β (β―βπ) β (1...(β―βπ))) |
12 | 10, 11 | sylib 217 |
. . . . 5
β’ (π β (β―βπ) β
(1...(β―βπ))) |
13 | | fz1fzo0m1 13626 |
. . . . 5
β’
((β―βπ)
β (1...(β―βπ)) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
14 | 12, 13 | syl 17 |
. . . 4
β’ (π β ((β―βπ) β 1) β
(0..^(β―βπ))) |
15 | 5, 14 | eqeltrd 2834 |
. . 3
β’ (π β π β (0..^(β―βπ))) |
16 | 1, 2, 3, 4, 15 | cycpmfvlem 32010 |
. 2
β’ (π β ((πΆβπ)β(πβπ)) = (((π cyclShift 1) β β‘π)β(πβπ))) |
17 | | df-f1 6502 |
. . . . 5
β’ (π:dom πβ1-1βπ· β (π:dom πβΆπ· β§ Fun β‘π)) |
18 | 4, 17 | sylib 217 |
. . . 4
β’ (π β (π:dom πβΆπ· β§ Fun β‘π)) |
19 | 18 | simprd 497 |
. . 3
β’ (π β Fun β‘π) |
20 | | wrdfn 14422 |
. . . . . 6
β’ (π β Word π· β π Fn (0..^(β―βπ))) |
21 | 3, 20 | syl 17 |
. . . . 5
β’ (π β π Fn (0..^(β―βπ))) |
22 | | fnfvelrn 7032 |
. . . . 5
β’ ((π Fn (0..^(β―βπ)) β§ π β (0..^(β―βπ))) β (πβπ) β ran π) |
23 | 21, 15, 22 | syl2anc 585 |
. . . 4
β’ (π β (πβπ) β ran π) |
24 | | df-rn 5645 |
. . . 4
β’ ran π = dom β‘π |
25 | 23, 24 | eleqtrdi 2844 |
. . 3
β’ (π β (πβπ) β dom β‘π) |
26 | | fvco 6940 |
. . 3
β’ ((Fun
β‘π β§ (πβπ) β dom β‘π) β (((π cyclShift 1) β β‘π)β(πβπ)) = ((π cyclShift 1)β(β‘πβ(πβπ)))) |
27 | 19, 25, 26 | syl2anc 585 |
. 2
β’ (π β (((π cyclShift 1) β β‘π)β(πβπ)) = ((π cyclShift 1)β(β‘πβ(πβπ)))) |
28 | | f1f1orn 6796 |
. . . . . 6
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
29 | 4, 28 | syl 17 |
. . . . 5
β’ (π β π:dom πβ1-1-ontoβran
π) |
30 | 21 | fndmd 6608 |
. . . . . 6
β’ (π β dom π = (0..^(β―βπ))) |
31 | 15, 30 | eleqtrrd 2837 |
. . . . 5
β’ (π β π β dom π) |
32 | | f1ocnvfv1 7223 |
. . . . 5
β’ ((π:dom πβ1-1-ontoβran
π β§ π β dom π) β (β‘πβ(πβπ)) = π) |
33 | 29, 31, 32 | syl2anc 585 |
. . . 4
β’ (π β (β‘πβ(πβπ)) = π) |
34 | 33 | fveq2d 6847 |
. . 3
β’ (π β ((π cyclShift 1)β(β‘πβ(πβπ))) = ((π cyclShift 1)βπ)) |
35 | | 1zzd 12539 |
. . . 4
β’ (π β 1 β
β€) |
36 | | cshwidxmod 14697 |
. . . 4
β’ ((π β Word π· β§ 1 β β€ β§ π β
(0..^(β―βπ)))
β ((π cyclShift
1)βπ) = (πβ((π + 1) mod (β―βπ)))) |
37 | 3, 35, 15, 36 | syl3anc 1372 |
. . 3
β’ (π β ((π cyclShift 1)βπ) = (πβ((π + 1) mod (β―βπ)))) |
38 | | fzossfz 13597 |
. . . . . . . 8
β’
(0..^(β―βπ)) β (0...(β―βπ)) |
39 | | fzssz 13449 |
. . . . . . . 8
β’
(0...(β―βπ)) β β€ |
40 | 38, 39 | sstri 3954 |
. . . . . . 7
β’
(0..^(β―βπ)) β β€ |
41 | 40, 15 | sselid 3943 |
. . . . . 6
β’ (π β π β β€) |
42 | 41 | zred 12612 |
. . . . 5
β’ (π β π β β) |
43 | 10 | nnrpd 12960 |
. . . . 5
β’ (π β (β―βπ) β
β+) |
44 | 5 | oveq1d 7373 |
. . . . . 6
β’ (π β (π mod (β―βπ)) = (((β―βπ) β 1) mod (β―βπ))) |
45 | | zmodidfzoimp 13812 |
. . . . . . 7
β’
(((β―βπ)
β 1) β (0..^(β―βπ)) β (((β―βπ) β 1) mod (β―βπ)) = ((β―βπ) β 1)) |
46 | 14, 45 | syl 17 |
. . . . . 6
β’ (π β (((β―βπ) β 1) mod
(β―βπ)) =
((β―βπ) β
1)) |
47 | 44, 46 | eqtrd 2773 |
. . . . 5
β’ (π β (π mod (β―βπ)) = ((β―βπ) β 1)) |
48 | | modm1p1mod0 13833 |
. . . . . 6
β’ ((π β β β§
(β―βπ) β
β+) β ((π mod (β―βπ)) = ((β―βπ) β 1) β ((π + 1) mod (β―βπ)) = 0)) |
49 | 48 | imp 408 |
. . . . 5
β’ (((π β β β§
(β―βπ) β
β+) β§ (π mod (β―βπ)) = ((β―βπ) β 1)) β ((π + 1) mod (β―βπ)) = 0) |
50 | 42, 43, 47, 49 | syl21anc 837 |
. . . 4
β’ (π β ((π + 1) mod (β―βπ)) = 0) |
51 | 50 | fveq2d 6847 |
. . 3
β’ (π β (πβ((π + 1) mod (β―βπ))) = (πβ0)) |
52 | 34, 37, 51 | 3eqtrd 2777 |
. 2
β’ (π β ((π cyclShift 1)β(β‘πβ(πβπ))) = (πβ0)) |
53 | 16, 27, 52 | 3eqtrd 2777 |
1
β’ (π β ((πΆβπ)β(πβπ)) = (πβ0)) |