Step | Hyp | Ref
| Expression |
1 | | tocycval.1 |
. . . 4
β’ πΆ = (toCycβπ·) |
2 | | tocycfv.d |
. . . 4
β’ (π β π· β π) |
3 | | tocycfv.w |
. . . 4
β’ (π β π β Word π·) |
4 | | tocycfv.1 |
. . . 4
β’ (π β π:dom πβ1-1βπ·) |
5 | 1, 2, 3, 4 | tocycfv 32007 |
. . 3
β’ (π β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) |
6 | 5 | fveq1d 6845 |
. 2
β’ (π β ((πΆβπ)βπ) = ((( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))βπ)) |
7 | | f1oi 6823 |
. . . 4
β’ ( I
βΎ (π· β ran
π)):(π· β ran π)β1-1-ontoβ(π· β ran π) |
8 | | f1ofn 6786 |
. . . 4
β’ (( I
βΎ (π· β ran
π)):(π· β ran π)β1-1-ontoβ(π· β ran π) β ( I βΎ (π· β ran π)) Fn (π· β ran π)) |
9 | 7, 8 | mp1i 13 |
. . 3
β’ (π β ( I βΎ (π· β ran π)) Fn (π· β ran π)) |
10 | | 1zzd 12539 |
. . . . . 6
β’ (π β 1 β
β€) |
11 | | cshwf 14694 |
. . . . . 6
β’ ((π β Word π· β§ 1 β β€) β (π cyclShift
1):(0..^(β―βπ))βΆπ·) |
12 | 3, 10, 11 | syl2anc 585 |
. . . . 5
β’ (π β (π cyclShift 1):(0..^(β―βπ))βΆπ·) |
13 | 12 | ffnd 6670 |
. . . 4
β’ (π β (π cyclShift 1) Fn (0..^(β―βπ))) |
14 | | df-f1 6502 |
. . . . . . . 8
β’ (π:dom πβ1-1βπ· β (π:dom πβΆπ· β§ Fun β‘π)) |
15 | 4, 14 | sylib 217 |
. . . . . . 7
β’ (π β (π:dom πβΆπ· β§ Fun β‘π)) |
16 | 15 | simprd 497 |
. . . . . 6
β’ (π β Fun β‘π) |
17 | 16 | funfnd 6533 |
. . . . 5
β’ (π β β‘π Fn dom β‘π) |
18 | | df-rn 5645 |
. . . . . 6
β’ ran π = dom β‘π |
19 | 18 | fneq2i 6601 |
. . . . 5
β’ (β‘π Fn ran π β β‘π Fn dom β‘π) |
20 | 17, 19 | sylibr 233 |
. . . 4
β’ (π β β‘π Fn ran π) |
21 | | dfdm4 5852 |
. . . . . 6
β’ dom π = ran β‘π |
22 | 21 | eqimss2i 4004 |
. . . . 5
β’ ran β‘π β dom π |
23 | | wrdfn 14422 |
. . . . . . 7
β’ (π β Word π· β π Fn (0..^(β―βπ))) |
24 | 3, 23 | syl 17 |
. . . . . 6
β’ (π β π Fn (0..^(β―βπ))) |
25 | 24 | fndmd 6608 |
. . . . 5
β’ (π β dom π = (0..^(β―βπ))) |
26 | 22, 25 | sseqtrid 3997 |
. . . 4
β’ (π β ran β‘π β (0..^(β―βπ))) |
27 | | fnco 6619 |
. . . 4
β’ (((π cyclShift 1) Fn
(0..^(β―βπ))
β§ β‘π Fn ran π β§ ran β‘π β (0..^(β―βπ))) β ((π cyclShift 1) β β‘π) Fn ran π) |
28 | 13, 20, 26, 27 | syl3anc 1372 |
. . 3
β’ (π β ((π cyclShift 1) β β‘π) Fn ran π) |
29 | | disjdifr 4433 |
. . . 4
β’ ((π· β ran π) β© ran π) = β
|
30 | 29 | a1i 11 |
. . 3
β’ (π β ((π· β ran π) β© ran π) = β
) |
31 | | cycpmfv3.1 |
. . . 4
β’ (π β π β π·) |
32 | | cycpmfv3.2 |
. . . 4
β’ (π β Β¬ π β ran π) |
33 | 31, 32 | eldifd 3922 |
. . 3
β’ (π β π β (π· β ran π)) |
34 | | fvun1 6933 |
. . 3
β’ ((( I
βΎ (π· β ran
π)) Fn (π· β ran π) β§ ((π cyclShift 1) β β‘π) Fn ran π β§ (((π· β ran π) β© ran π) = β
β§ π β (π· β ran π))) β ((( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))βπ) = (( I βΎ (π· β ran π))βπ)) |
35 | 9, 28, 30, 33, 34 | syl112anc 1375 |
. 2
β’ (π β ((( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))βπ) = (( I βΎ (π· β ran π))βπ)) |
36 | | fvresi 7120 |
. . 3
β’ (π β (π· β ran π) β (( I βΎ (π· β ran π))βπ) = π) |
37 | 33, 36 | syl 17 |
. 2
β’ (π β (( I βΎ (π· β ran π))βπ) = π) |
38 | 6, 35, 37 | 3eqtrd 2777 |
1
β’ (π β ((πΆβπ)βπ) = π) |