Step | Hyp | Ref
| Expression |
1 | | resco 6203 |
. . . . 5
β’ ((β‘π β (πβπ)) βΎ ran π) = (β‘π β ((πβπ) βΎ ran π)) |
2 | 1 | coeq1i 5816 |
. . . 4
β’ (((β‘π β (πβπ)) βΎ ran π) β π) = ((β‘π β ((πβπ) βΎ ran π)) β π) |
3 | | ssid 3967 |
. . . . 5
β’ ran π β ran π |
4 | | cores 6202 |
. . . . 5
β’ (ran
π β ran π β (((β‘π β (πβπ)) βΎ ran π) β π) = ((β‘π β (πβπ)) β π)) |
5 | 3, 4 | ax-mp 5 |
. . . 4
β’ (((β‘π β (πβπ)) βΎ ran π) β π) = ((β‘π β (πβπ)) β π) |
6 | | coass 6218 |
. . . 4
β’ ((β‘π β ((πβπ) βΎ ran π)) β π) = (β‘π β (((πβπ) βΎ ran π) β π)) |
7 | 2, 5, 6 | 3eqtr3i 2769 |
. . 3
β’ ((β‘π β (πβπ)) β π) = (β‘π β (((πβπ) βΎ ran π) β π)) |
8 | | cycpmconjs.m |
. . . . . . 7
β’ π = (toCycβπ·) |
9 | | cycpmconjslem1.d |
. . . . . . 7
β’ (π β π· β π) |
10 | | cycpmconjslem1.w |
. . . . . . 7
β’ (π β π β Word π·) |
11 | | cycpmconjslem1.1 |
. . . . . . 7
β’ (π β π:dom πβ1-1βπ·) |
12 | 8, 9, 10, 11 | tocycfvres1 32008 |
. . . . . 6
β’ (π β ((πβπ) βΎ ran π) = ((π cyclShift 1) β β‘π)) |
13 | 12 | coeq1d 5818 |
. . . . 5
β’ (π β (((πβπ) βΎ ran π) β π) = (((π cyclShift 1) β β‘π) β π)) |
14 | | coass 6218 |
. . . . . 6
β’ (((π cyclShift 1) β β‘π) β π) = ((π cyclShift 1) β (β‘π β π)) |
15 | | f1f1orn 6796 |
. . . . . . . . 9
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
16 | | f1ococnv1 6814 |
. . . . . . . . 9
β’ (π:dom πβ1-1-ontoβran
π β (β‘π β π) = ( I βΎ dom π)) |
17 | 11, 15, 16 | 3syl 18 |
. . . . . . . 8
β’ (π β (β‘π β π) = ( I βΎ dom π)) |
18 | 17 | coeq2d 5819 |
. . . . . . 7
β’ (π β ((π cyclShift 1) β (β‘π β π)) = ((π cyclShift 1) β ( I βΎ dom π))) |
19 | | coires1 6217 |
. . . . . . 7
β’ ((π cyclShift 1) β ( I
βΎ dom π)) = ((π cyclShift 1) βΎ dom π) |
20 | 18, 19 | eqtr2di 2790 |
. . . . . 6
β’ (π β ((π cyclShift 1) βΎ dom π) = ((π cyclShift 1) β (β‘π β π))) |
21 | 14, 20 | eqtr4id 2792 |
. . . . 5
β’ (π β (((π cyclShift 1) β β‘π) β π) = ((π cyclShift 1) βΎ dom π)) |
22 | | 1zzd 12539 |
. . . . . . . 8
β’ (π β 1 β
β€) |
23 | | cshwfn 14695 |
. . . . . . . 8
β’ ((π β Word π· β§ 1 β β€) β (π cyclShift 1) Fn
(0..^(β―βπ))) |
24 | 10, 22, 23 | syl2anc 585 |
. . . . . . 7
β’ (π β (π cyclShift 1) Fn (0..^(β―βπ))) |
25 | | wrddm 14415 |
. . . . . . . . 9
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
26 | 10, 25 | syl 17 |
. . . . . . . 8
β’ (π β dom π = (0..^(β―βπ))) |
27 | 26 | fneq2d 6597 |
. . . . . . 7
β’ (π β ((π cyclShift 1) Fn dom π β (π cyclShift 1) Fn (0..^(β―βπ)))) |
28 | 24, 27 | mpbird 257 |
. . . . . 6
β’ (π β (π cyclShift 1) Fn dom π) |
29 | | fnresdm 6621 |
. . . . . 6
β’ ((π cyclShift 1) Fn dom π β ((π cyclShift 1) βΎ dom π) = (π cyclShift 1)) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ (π β ((π cyclShift 1) βΎ dom π) = (π cyclShift 1)) |
31 | 13, 21, 30 | 3eqtrd 2777 |
. . . 4
β’ (π β (((πβπ) βΎ ran π) β π) = (π cyclShift 1)) |
32 | 31 | coeq2d 5819 |
. . 3
β’ (π β (β‘π β (((πβπ) βΎ ran π) β π)) = (β‘π β (π cyclShift 1))) |
33 | 7, 32 | eqtrid 2785 |
. 2
β’ (π β ((β‘π β (πβπ)) β π) = (β‘π β (π cyclShift 1))) |
34 | | wrdfn 14422 |
. . . . . 6
β’ (π β Word π· β π Fn (0..^(β―βπ))) |
35 | 10, 34 | syl 17 |
. . . . 5
β’ (π β π Fn (0..^(β―βπ))) |
36 | | df-f 6501 |
. . . . 5
β’ (π:(0..^(β―βπ))βΆran π β (π Fn (0..^(β―βπ)) β§ ran π β ran π)) |
37 | 35, 3, 36 | sylanblrc 591 |
. . . 4
β’ (π β π:(0..^(β―βπ))βΆran π) |
38 | | iswrdi 14412 |
. . . 4
β’ (π:(0..^(β―βπ))βΆran π β π β Word ran π) |
39 | 37, 38 | syl 17 |
. . 3
β’ (π β π β Word ran π) |
40 | | f1ocnv 6797 |
. . . . 5
β’ (π:dom πβ1-1-ontoβran
π β β‘π:ran πβ1-1-ontoβdom
π) |
41 | 11, 15, 40 | 3syl 18 |
. . . 4
β’ (π β β‘π:ran πβ1-1-ontoβdom
π) |
42 | | f1of 6785 |
. . . 4
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
43 | 41, 42 | syl 17 |
. . 3
β’ (π β β‘π:ran πβΆdom π) |
44 | | cshco 14731 |
. . 3
β’ ((π β Word ran π β§ 1 β β€ β§
β‘π:ran πβΆdom π) β (β‘π β (π cyclShift 1)) = ((β‘π β π) cyclShift 1)) |
45 | 39, 22, 43, 44 | syl3anc 1372 |
. 2
β’ (π β (β‘π β (π cyclShift 1)) = ((β‘π β π) cyclShift 1)) |
46 | | cycpmconjslem1.2 |
. . . . . . 7
β’ (π β (β―βπ) = π) |
47 | 46 | oveq2d 7374 |
. . . . . 6
β’ (π β (0..^(β―βπ)) = (0..^π)) |
48 | 26, 47 | eqtrd 2773 |
. . . . 5
β’ (π β dom π = (0..^π)) |
49 | 48 | reseq2d 5938 |
. . . 4
β’ (π β ( I βΎ dom π) = ( I βΎ (0..^π))) |
50 | 17, 49 | eqtrd 2773 |
. . 3
β’ (π β (β‘π β π) = ( I βΎ (0..^π))) |
51 | 50 | oveq1d 7373 |
. 2
β’ (π β ((β‘π β π) cyclShift 1) = (( I βΎ (0..^π)) cyclShift
1)) |
52 | 33, 45, 51 | 3eqtrd 2777 |
1
β’ (π β ((β‘π β (πβπ)) β π) = (( I βΎ (0..^π)) cyclShift 1)) |