Step | Hyp | Ref
| Expression |
1 | | tocyc01.1 |
. . . . 5
β’ πΆ = (toCycβπ·) |
2 | | simpl 484 |
. . . . 5
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π· β π) |
3 | | simpr 486 |
. . . . . . . . 9
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π β (dom πΆ β© (β‘β― β {0, 1}))) |
4 | 3 | elin1d 4159 |
. . . . . . . 8
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π β dom πΆ) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’
(SymGrpβπ·) =
(SymGrpβπ·) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβ(SymGrpβπ·)) = (Baseβ(SymGrpβπ·)) |
7 | 1, 5, 6 | tocycf 32015 |
. . . . . . . . 9
β’ (π· β π β πΆ:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβ(SymGrpβπ·))) |
8 | | fdm 6678 |
. . . . . . . . 9
β’ (πΆ:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβ(SymGrpβπ·)) β dom πΆ = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
9 | 2, 7, 8 | 3syl 18 |
. . . . . . . 8
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β dom πΆ = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
10 | 4, 9 | eleqtrd 2836 |
. . . . . . 7
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
11 | | id 22 |
. . . . . . . . 9
β’ (π€ = π β π€ = π) |
12 | | dmeq 5860 |
. . . . . . . . 9
β’ (π€ = π β dom π€ = dom π) |
13 | | eqidd 2734 |
. . . . . . . . 9
β’ (π€ = π β π· = π·) |
14 | 11, 12, 13 | f1eq123d 6777 |
. . . . . . . 8
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
15 | 14 | elrab 3646 |
. . . . . . 7
β’ (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π β Word π· β§ π:dom πβ1-1βπ·)) |
16 | 10, 15 | sylib 217 |
. . . . . 6
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β (π β Word π· β§ π:dom πβ1-1βπ·)) |
17 | 16 | simpld 496 |
. . . . 5
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π β Word π·) |
18 | 16 | simprd 497 |
. . . . 5
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π:dom πβ1-1βπ·) |
19 | 1, 2, 17, 18 | tocycfv 32007 |
. . . 4
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) |
20 | 19 | adantr 482 |
. . 3
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 0)
β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) |
21 | | hasheq0 14269 |
. . . . . 6
β’ (π β (dom πΆ β© (β‘β― β {0, 1})) β
((β―βπ) = 0
β π =
β
)) |
22 | 3, 21 | syl 17 |
. . . . 5
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β
((β―βπ) = 0
β π =
β
)) |
23 | 22 | biimpa 478 |
. . . 4
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 0)
β π =
β
) |
24 | | rneq 5892 |
. . . . . . . . . 10
β’ (π = β
β ran π = ran β
) |
25 | | rn0 5882 |
. . . . . . . . . 10
β’ ran
β
= β
|
26 | 24, 25 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π = β
β ran π = β
) |
27 | 26 | difeq2d 4083 |
. . . . . . . 8
β’ (π = β
β (π· β ran π) = (π· β β
)) |
28 | | dif0 4333 |
. . . . . . . 8
β’ (π· β β
) = π· |
29 | 27, 28 | eqtrdi 2789 |
. . . . . . 7
β’ (π = β
β (π· β ran π) = π·) |
30 | 29 | reseq2d 5938 |
. . . . . 6
β’ (π = β
β ( I βΎ
(π· β ran π)) = ( I βΎ π·)) |
31 | | cnveq 5830 |
. . . . . . . . 9
β’ (π = β
β β‘π = β‘β
) |
32 | | cnv0 6094 |
. . . . . . . . 9
β’ β‘β
= β
|
33 | 31, 32 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = β
β β‘π = β
) |
34 | 33 | coeq2d 5819 |
. . . . . . 7
β’ (π = β
β ((π cyclShift 1) β β‘π) = ((π cyclShift 1) β
β
)) |
35 | | co02 6213 |
. . . . . . 7
β’ ((π cyclShift 1) β β
) =
β
|
36 | 34, 35 | eqtrdi 2789 |
. . . . . 6
β’ (π = β
β ((π cyclShift 1) β β‘π) = β
) |
37 | 30, 36 | uneq12d 4125 |
. . . . 5
β’ (π = β
β (( I βΎ
(π· β ran π)) βͺ ((π cyclShift 1) β β‘π)) = (( I βΎ π·) βͺ β
)) |
38 | | un0 4351 |
. . . . 5
β’ (( I
βΎ π·) βͺ β
) =
( I βΎ π·) |
39 | 37, 38 | eqtrdi 2789 |
. . . 4
β’ (π = β
β (( I βΎ
(π· β ran π)) βͺ ((π cyclShift 1) β β‘π)) = ( I βΎ π·)) |
40 | 23, 39 | syl 17 |
. . 3
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 0)
β (( I βΎ (π·
β ran π)) βͺ
((π cyclShift 1) β
β‘π)) = ( I βΎ π·)) |
41 | 20, 40 | eqtrd 2773 |
. 2
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 0)
β (πΆβπ) = ( I βΎ π·)) |
42 | 19 | adantr 482 |
. . 3
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) |
43 | 17 | adantr 482 |
. . . . . . 7
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β π β Word π·) |
44 | | 1zzd 12539 |
. . . . . . 7
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β 1 β β€) |
45 | | simpr 486 |
. . . . . . 7
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (β―βπ) =
1) |
46 | | 1cshid 31862 |
. . . . . . 7
β’ ((π β Word π· β§ 1 β β€ β§
(β―βπ) = 1)
β (π cyclShift 1) =
π) |
47 | 43, 44, 45, 46 | syl3anc 1372 |
. . . . . 6
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (π cyclShift 1) =
π) |
48 | 47 | coeq1d 5818 |
. . . . 5
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β ((π cyclShift 1)
β β‘π) = (π β β‘π)) |
49 | | wrdf 14413 |
. . . . . 6
β’ (π β Word π· β π:(0..^(β―βπ))βΆπ·) |
50 | | ffun 6672 |
. . . . . 6
β’ (π:(0..^(β―βπ))βΆπ· β Fun π) |
51 | | funcocnv2 6810 |
. . . . . 6
β’ (Fun
π β (π β β‘π) = ( I βΎ ran π)) |
52 | 43, 49, 50, 51 | 4syl 19 |
. . . . 5
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (π β β‘π) = ( I βΎ ran π)) |
53 | 48, 52 | eqtrd 2773 |
. . . 4
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β ((π cyclShift 1)
β β‘π) = ( I βΎ ran π)) |
54 | 53 | uneq2d 4124 |
. . 3
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (( I βΎ (π·
β ran π)) βͺ
((π cyclShift 1) β
β‘π)) = (( I βΎ (π· β ran π)) βͺ ( I βΎ ran π))) |
55 | | resundi 5952 |
. . . 4
β’ ( I
βΎ ((π· β ran
π) βͺ ran π)) = (( I βΎ (π· β ran π)) βͺ ( I βΎ ran π)) |
56 | | frn 6676 |
. . . . . . 7
β’ (π:(0..^(β―βπ))βΆπ· β ran π β π·) |
57 | | undifr 31494 |
. . . . . . 7
β’ (ran
π β π· β ((π· β ran π) βͺ ran π) = π·) |
58 | 56, 57 | sylib 217 |
. . . . . 6
β’ (π:(0..^(β―βπ))βΆπ· β ((π· β ran π) βͺ ran π) = π·) |
59 | 43, 49, 58 | 3syl 18 |
. . . . 5
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β ((π· β ran
π) βͺ ran π) = π·) |
60 | 59 | reseq2d 5938 |
. . . 4
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β ( I βΎ ((π·
β ran π) βͺ ran
π)) = ( I βΎ π·)) |
61 | 55, 60 | eqtr3id 2787 |
. . 3
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (( I βΎ (π·
β ran π)) βͺ ( I
βΎ ran π)) = ( I
βΎ π·)) |
62 | 42, 54, 61 | 3eqtrd 2777 |
. 2
β’ (((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β§
(β―βπ) = 1)
β (πΆβπ) = ( I βΎ π·)) |
63 | 3 | elin2d 4160 |
. . . . 5
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β π β (β‘β― β {0, 1})) |
64 | | hashf 14244 |
. . . . . 6
β’
β―:VβΆ(β0 βͺ {+β}) |
65 | | ffn 6669 |
. . . . . 6
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
66 | | elpreima 7009 |
. . . . . 6
β’ (β―
Fn V β (π β
(β‘β― β {0, 1}) β (π β V β§
(β―βπ) β
{0, 1}))) |
67 | 64, 65, 66 | mp2b 10 |
. . . . 5
β’ (π β (β‘β― β {0, 1}) β (π β V β§
(β―βπ) β
{0, 1})) |
68 | 63, 67 | sylib 217 |
. . . 4
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β (π β V β§
(β―βπ) β
{0, 1})) |
69 | 68 | simprd 497 |
. . 3
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β
(β―βπ) β
{0, 1}) |
70 | | elpri 4609 |
. . 3
β’
((β―βπ)
β {0, 1} β ((β―βπ) = 0 β¨ (β―βπ) = 1)) |
71 | 69, 70 | syl 17 |
. 2
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β
((β―βπ) = 0 β¨
(β―βπ) =
1)) |
72 | 41, 62, 71 | mpjaodan 958 |
1
β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β (πΆβπ) = ( I βΎ π·)) |