Step | Hyp | Ref
| Expression |
1 | | f1oi 6823 |
. . . . 5
β’ ( I
βΎ (π· β ran
π)):(π· β ran π)β1-1-ontoβ(π· β ran π) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β ( I βΎ (π· β ran π)):(π· β ran π)β1-1-ontoβ(π· β ran π)) |
3 | | tocycfv.w |
. . . . . . . . 9
β’ (π β π β Word π·) |
4 | | 1zzd 12539 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
5 | | cshwf 14694 |
. . . . . . . . 9
β’ ((π β Word π· β§ 1 β β€) β (π cyclShift
1):(0..^(β―βπ))βΆπ·) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π cyclShift 1):(0..^(β―βπ))βΆπ·) |
7 | 6 | ffnd 6670 |
. . . . . . 7
β’ (π β (π cyclShift 1) Fn (0..^(β―βπ))) |
8 | | tocycfv.1 |
. . . . . . . . . 10
β’ (π β π:dom πβ1-1βπ·) |
9 | | df-f1 6502 |
. . . . . . . . . 10
β’ (π:dom πβ1-1βπ· β (π:dom πβΆπ· β§ Fun β‘π)) |
10 | 8, 9 | sylib 217 |
. . . . . . . . 9
β’ (π β (π:dom πβΆπ· β§ Fun β‘π)) |
11 | 10 | simprd 497 |
. . . . . . . 8
β’ (π β Fun β‘π) |
12 | | eqid 2733 |
. . . . . . . . 9
β’ (π cyclShift 1) = (π cyclShift 1) |
13 | | cshinj 14705 |
. . . . . . . . 9
β’ ((π β Word π· β§ Fun β‘π β§ 1 β β€) β ((π cyclShift 1) = (π cyclShift 1) β Fun β‘(π cyclShift 1))) |
14 | 12, 13 | mpi 20 |
. . . . . . . 8
β’ ((π β Word π· β§ Fun β‘π β§ 1 β β€) β Fun β‘(π cyclShift 1)) |
15 | 3, 11, 4, 14 | syl3anc 1372 |
. . . . . . 7
β’ (π β Fun β‘(π cyclShift 1)) |
16 | | f1orn 6795 |
. . . . . . 7
β’ ((π cyclShift
1):(0..^(β―βπ))β1-1-ontoβran
(π cyclShift 1) β
((π cyclShift 1) Fn
(0..^(β―βπ))
β§ Fun β‘(π cyclShift 1))) |
17 | 7, 15, 16 | sylanbrc 584 |
. . . . . 6
β’ (π β (π cyclShift 1):(0..^(β―βπ))β1-1-ontoβran
(π cyclShift
1)) |
18 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π cyclShift 1) = (π cyclShift 1)) |
19 | | wrdf 14413 |
. . . . . . . . 9
β’ (π β Word π· β π:(0..^(β―βπ))βΆπ·) |
20 | 3, 19 | syl 17 |
. . . . . . . 8
β’ (π β π:(0..^(β―βπ))βΆπ·) |
21 | 20 | fdmd 6680 |
. . . . . . 7
β’ (π β dom π = (0..^(β―βπ))) |
22 | | cshwrnid 31864 |
. . . . . . . . 9
β’ ((π β Word π· β§ 1 β β€) β ran (π cyclShift 1) = ran π) |
23 | 3, 4, 22 | syl2anc 585 |
. . . . . . . 8
β’ (π β ran (π cyclShift 1) = ran π) |
24 | 23 | eqcomd 2739 |
. . . . . . 7
β’ (π β ran π = ran (π cyclShift 1)) |
25 | 18, 21, 24 | f1oeq123d 6779 |
. . . . . 6
β’ (π β ((π cyclShift 1):dom πβ1-1-ontoβran
π β (π cyclShift 1):(0..^(β―βπ))β1-1-ontoβran
(π cyclShift
1))) |
26 | 17, 25 | mpbird 257 |
. . . . 5
β’ (π β (π cyclShift 1):dom πβ1-1-ontoβran
π) |
27 | | f1f1orn 6796 |
. . . . . 6
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
28 | | f1ocnv 6797 |
. . . . . 6
β’ (π:dom πβ1-1-ontoβran
π β β‘π:ran πβ1-1-ontoβdom
π) |
29 | 8, 27, 28 | 3syl 18 |
. . . . 5
β’ (π β β‘π:ran πβ1-1-ontoβdom
π) |
30 | | f1oco 6808 |
. . . . 5
β’ (((π cyclShift 1):dom πβ1-1-ontoβran
π β§ β‘π:ran πβ1-1-ontoβdom
π) β ((π cyclShift 1) β β‘π):ran πβ1-1-ontoβran
π) |
31 | 26, 29, 30 | syl2anc 585 |
. . . 4
β’ (π β ((π cyclShift 1) β β‘π):ran πβ1-1-ontoβran
π) |
32 | | disjdifr 4433 |
. . . . 5
β’ ((π· β ran π) β© ran π) = β
|
33 | 32 | a1i 11 |
. . . 4
β’ (π β ((π· β ran π) β© ran π) = β
) |
34 | | f1oun 6804 |
. . . 4
β’ (((( I
βΎ (π· β ran
π)):(π· β ran π)β1-1-ontoβ(π· β ran π) β§ ((π cyclShift 1) β β‘π):ran πβ1-1-ontoβran
π) β§ (((π· β ran π) β© ran π) = β
β§ ((π· β ran π) β© ran π) = β
)) β (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π)):((π· β ran π) βͺ ran π)β1-1-ontoβ((π· β ran π) βͺ ran π)) |
35 | 2, 31, 33, 33, 34 | syl22anc 838 |
. . 3
β’ (π β (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π)):((π· β ran π) βͺ ran π)β1-1-ontoβ((π· β ran π) βͺ ran π)) |
36 | | tocycval.1 |
. . . . 5
β’ πΆ = (toCycβπ·) |
37 | | tocycfv.d |
. . . . 5
β’ (π β π· β π) |
38 | 36, 37, 3, 8 | tocycfv 32007 |
. . . 4
β’ (π β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) |
39 | 20 | frnd 6677 |
. . . . . 6
β’ (π β ran π β π·) |
40 | | undif 4442 |
. . . . . 6
β’ (ran
π β π· β (ran π βͺ (π· β ran π)) = π·) |
41 | 39, 40 | sylib 217 |
. . . . 5
β’ (π β (ran π βͺ (π· β ran π)) = π·) |
42 | | uncom 4114 |
. . . . 5
β’ (ran
π βͺ (π· β ran π)) = ((π· β ran π) βͺ ran π) |
43 | 41, 42 | eqtr3di 2788 |
. . . 4
β’ (π β π· = ((π· β ran π) βͺ ran π)) |
44 | 38, 43, 43 | f1oeq123d 6779 |
. . 3
β’ (π β ((πΆβπ):π·β1-1-ontoβπ· β (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π)):((π· β ran π) βͺ ran π)β1-1-ontoβ((π· β ran π) βͺ ran π))) |
45 | 35, 44 | mpbird 257 |
. 2
β’ (π β (πΆβπ):π·β1-1-ontoβπ·) |
46 | | fvex 6856 |
. . 3
β’ (πΆβπ) β V |
47 | | cycpmcl.s |
. . . 4
β’ π = (SymGrpβπ·) |
48 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
49 | 47, 48 | elsymgbas2 19159 |
. . 3
β’ ((πΆβπ) β V β ((πΆβπ) β (Baseβπ) β (πΆβπ):π·β1-1-ontoβπ·)) |
50 | 46, 49 | ax-mp 5 |
. 2
β’ ((πΆβπ) β (Baseβπ) β (πΆβπ):π·β1-1-ontoβπ·) |
51 | 45, 50 | sylibr 233 |
1
β’ (π β (πΆβπ) β (Baseβπ)) |