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 | | lencl 14427 |
. . . . . . 7
β’ (π β Word π· β (β―βπ) β
β0) |
6 | 3, 5 | syl 17 |
. . . . . 6
β’ (π β (β―βπ) β
β0) |
7 | 6 | nn0zd 12530 |
. . . . 5
β’ (π β (β―βπ) β
β€) |
8 | | fzossrbm1 13607 |
. . . . 5
β’
((β―βπ)
β β€ β (0..^((β―βπ) β 1)) β
(0..^(β―βπ))) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (π β (0..^((β―βπ) β 1)) β
(0..^(β―βπ))) |
10 | | cycpmfv1.1 |
. . . 4
β’ (π β π β (0..^((β―βπ) β 1))) |
11 | 9, 10 | sseldd 3946 |
. . 3
β’ (π β π β (0..^(β―βπ))) |
12 | 1, 2, 3, 4, 11 | cycpmfvlem 32010 |
. 2
β’ (π β ((πΆβπ)β(πβπ)) = (((π cyclShift 1) β β‘π)β(πβπ))) |
13 | | df-f1 6502 |
. . . . 5
β’ (π:dom πβ1-1βπ· β (π:dom πβΆπ· β§ Fun β‘π)) |
14 | 4, 13 | sylib 217 |
. . . 4
β’ (π β (π:dom πβΆπ· β§ Fun β‘π)) |
15 | 14 | simprd 497 |
. . 3
β’ (π β Fun β‘π) |
16 | | wrdfn 14422 |
. . . . . 6
β’ (π β Word π· β π Fn (0..^(β―βπ))) |
17 | 3, 16 | syl 17 |
. . . . 5
β’ (π β π Fn (0..^(β―βπ))) |
18 | | fnfvelrn 7032 |
. . . . 5
β’ ((π Fn (0..^(β―βπ)) β§ π β (0..^(β―βπ))) β (πβπ) β ran π) |
19 | 17, 11, 18 | syl2anc 585 |
. . . 4
β’ (π β (πβπ) β ran π) |
20 | | df-rn 5645 |
. . . 4
β’ ran π = dom β‘π |
21 | 19, 20 | eleqtrdi 2844 |
. . 3
β’ (π β (πβπ) β dom β‘π) |
22 | | fvco 6940 |
. . 3
β’ ((Fun
β‘π β§ (πβπ) β dom β‘π) β (((π cyclShift 1) β β‘π)β(πβπ)) = ((π cyclShift 1)β(β‘πβ(πβπ)))) |
23 | 15, 21, 22 | syl2anc 585 |
. 2
β’ (π β (((π cyclShift 1) β β‘π)β(πβπ)) = ((π cyclShift 1)β(β‘πβ(πβπ)))) |
24 | | f1f1orn 6796 |
. . . . . 6
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
25 | 4, 24 | syl 17 |
. . . . 5
β’ (π β π:dom πβ1-1-ontoβran
π) |
26 | 17 | fndmd 6608 |
. . . . . 6
β’ (π β dom π = (0..^(β―βπ))) |
27 | 11, 26 | eleqtrrd 2837 |
. . . . 5
β’ (π β π β dom π) |
28 | | f1ocnvfv1 7223 |
. . . . 5
β’ ((π:dom πβ1-1-ontoβran
π β§ π β dom π) β (β‘πβ(πβπ)) = π) |
29 | 25, 27, 28 | syl2anc 585 |
. . . 4
β’ (π β (β‘πβ(πβπ)) = π) |
30 | 29 | fveq2d 6847 |
. . 3
β’ (π β ((π cyclShift 1)β(β‘πβ(πβπ))) = ((π cyclShift 1)βπ)) |
31 | | 1zzd 12539 |
. . . 4
β’ (π β 1 β
β€) |
32 | | cshwidxmod 14697 |
. . . 4
β’ ((π β Word π· β§ 1 β β€ β§ π β
(0..^(β―βπ)))
β ((π cyclShift
1)βπ) = (πβ((π + 1) mod (β―βπ)))) |
33 | 3, 31, 11, 32 | syl3anc 1372 |
. . 3
β’ (π β ((π cyclShift 1)βπ) = (πβ((π + 1) mod (β―βπ)))) |
34 | | fzo0ss1 13608 |
. . . . . 6
β’
(1..^(β―βπ)) β (0..^(β―βπ)) |
35 | | fzoaddel2 13634 |
. . . . . . 7
β’ ((π β
(0..^((β―βπ)
β 1)) β§ (β―βπ) β β€ β§ 1 β β€)
β (π + 1) β
(1..^(β―βπ))) |
36 | 10, 7, 31, 35 | syl3anc 1372 |
. . . . . 6
β’ (π β (π + 1) β (1..^(β―βπ))) |
37 | 34, 36 | sselid 3943 |
. . . . 5
β’ (π β (π + 1) β (0..^(β―βπ))) |
38 | | zmodidfzoimp 13812 |
. . . . 5
β’ ((π + 1) β
(0..^(β―βπ))
β ((π + 1) mod
(β―βπ)) = (π + 1)) |
39 | 37, 38 | syl 17 |
. . . 4
β’ (π β ((π + 1) mod (β―βπ)) = (π + 1)) |
40 | 39 | fveq2d 6847 |
. . 3
β’ (π β (πβ((π + 1) mod (β―βπ))) = (πβ(π + 1))) |
41 | 30, 33, 40 | 3eqtrd 2777 |
. 2
β’ (π β ((π cyclShift 1)β(β‘πβ(πβπ))) = (πβ(π + 1))) |
42 | 12, 23, 41 | 3eqtrd 2777 |
1
β’ (π β ((πΆβπ)β(πβπ)) = (πβ(π + 1))) |