Step | Hyp | Ref
| Expression |
1 | | tocycf.c |
. . 3
β’ πΆ = (toCycβπ·) |
2 | 1 | tocycval 32006 |
. 2
β’ (π· β π β πΆ = (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β¦ (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)))) |
3 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β π’ = β
) |
4 | 3 | rneqd 5894 |
. . . . . . . . . 10
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ran π’ = ran β
) |
5 | | rn0 5882 |
. . . . . . . . . 10
β’ ran
β
= β
|
6 | 4, 5 | eqtrdi 2789 |
. . . . . . . . 9
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ran π’ = β
) |
7 | 6 | difeq2d 4083 |
. . . . . . . 8
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β (π· β ran π’) = (π· β β
)) |
8 | | dif0 4333 |
. . . . . . . 8
β’ (π· β β
) = π· |
9 | 7, 8 | eqtrdi 2789 |
. . . . . . 7
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β (π· β ran π’) = π·) |
10 | 9 | reseq2d 5938 |
. . . . . 6
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ( I βΎ (π· β ran π’)) = ( I βΎ π·)) |
11 | 3 | cnveqd 5832 |
. . . . . . . . 9
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β β‘π’ = β‘β
) |
12 | | cnv0 6094 |
. . . . . . . . 9
β’ β‘β
= β
|
13 | 11, 12 | eqtrdi 2789 |
. . . . . . . 8
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β β‘π’ = β
) |
14 | 13 | coeq2d 5819 |
. . . . . . 7
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ((π’ cyclShift 1) β β‘π’) = ((π’ cyclShift 1) β
β
)) |
15 | | co02 6213 |
. . . . . . 7
β’ ((π’ cyclShift 1) β β
) =
β
|
16 | 14, 15 | eqtrdi 2789 |
. . . . . 6
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ((π’ cyclShift 1) β β‘π’) = β
) |
17 | 10, 16 | uneq12d 4125 |
. . . . 5
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) = (( I βΎ π·) βͺ β
)) |
18 | | un0 4351 |
. . . . 5
β’ (( I
βΎ π·) βͺ β
) =
( I βΎ π·) |
19 | 17, 18 | eqtrdi 2789 |
. . . 4
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) = ( I βΎ π·)) |
20 | | tocycf.s |
. . . . . . 7
β’ π = (SymGrpβπ·) |
21 | 20 | idresperm 19172 |
. . . . . 6
β’ (π· β π β ( I βΎ π·) β (Baseβπ)) |
22 | | tocycf.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
23 | 21, 22 | eleqtrrdi 2845 |
. . . . 5
β’ (π· β π β ( I βΎ π·) β π΅) |
24 | 23 | ad2antrr 725 |
. . . 4
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β ( I βΎ π·) β π΅) |
25 | 19, 24 | eqeltrd 2834 |
. . 3
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ = β
) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β π΅) |
26 | | difexg 5285 |
. . . . . . . . 9
β’ (π· β π β (π· β ran π’) β V) |
27 | 26 | resiexd 7167 |
. . . . . . . 8
β’ (π· β π β ( I βΎ (π· β ran π’)) β V) |
28 | | ovex 7391 |
. . . . . . . . 9
β’ (π’ cyclShift 1) β
V |
29 | | vex 3448 |
. . . . . . . . . 10
β’ π’ β V |
30 | 29 | cnvex 7863 |
. . . . . . . . 9
β’ β‘π’ β V |
31 | 28, 30 | coex 7868 |
. . . . . . . 8
β’ ((π’ cyclShift 1) β β‘π’) β V |
32 | | unexg 7684 |
. . . . . . . 8
β’ ((( I
βΎ (π· β ran
π’)) β V β§ ((π’ cyclShift 1) β β‘π’) β V) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β V) |
33 | 27, 31, 32 | sylancl 587 |
. . . . . . 7
β’ (π· β π β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β V) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β V) |
35 | 2, 34 | fvmpt2d 6962 |
. . . . 5
β’ ((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β (πΆβπ’) = (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’))) |
36 | 35 | adantr 482 |
. . . 4
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β (πΆβπ’) = (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’))) |
37 | | simpll 766 |
. . . . . 6
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β π· β π) |
38 | | simplr 768 |
. . . . . . . 8
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
39 | | id 22 |
. . . . . . . . . 10
β’ (π€ = π’ β π€ = π’) |
40 | | dmeq 5860 |
. . . . . . . . . 10
β’ (π€ = π’ β dom π€ = dom π’) |
41 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π€ = π’ β π· = π·) |
42 | 39, 40, 41 | f1eq123d 6777 |
. . . . . . . . 9
β’ (π€ = π’ β (π€:dom π€β1-1βπ· β π’:dom π’β1-1βπ·)) |
43 | 42 | elrab 3646 |
. . . . . . . 8
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π’ β Word π· β§ π’:dom π’β1-1βπ·)) |
44 | 38, 43 | sylib 217 |
. . . . . . 7
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β (π’ β Word π· β§ π’:dom π’β1-1βπ·)) |
45 | 44 | simpld 496 |
. . . . . 6
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β π’ β Word π·) |
46 | 44 | simprd 497 |
. . . . . 6
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β π’:dom π’β1-1βπ·) |
47 | 1, 37, 45, 46, 20 | cycpmcl 32014 |
. . . . 5
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β (πΆβπ’) β (Baseβπ)) |
48 | 47, 22 | eleqtrrdi 2845 |
. . . 4
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β (πΆβπ’) β π΅) |
49 | 36, 48 | eqeltrrd 2835 |
. . 3
β’ (((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β§ π’ β β
) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β π΅) |
50 | 25, 49 | pm2.61dane 3029 |
. 2
β’ ((π· β π β§ π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β (( I βΎ (π· β ran π’)) βͺ ((π’ cyclShift 1) β β‘π’)) β π΅) |
51 | 2, 50 | fmpt3d 7065 |
1
β’ (π· β π β πΆ:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅) |