Step | Hyp | Ref
| Expression |
1 | | cycpmco2.d |
. . 3
β’ (π β π· β π) |
2 | | ssrab2 4038 |
. . . . . 6
β’ {π€ β Word π· β£ π€:dom π€β1-1βπ·} β Word π· |
3 | | cycpmco2.w |
. . . . . . 7
β’ (π β π β dom π) |
4 | | cycpmco2.c |
. . . . . . . . . 10
β’ π = (toCycβπ·) |
5 | | cycpmco2.s |
. . . . . . . . . 10
β’ π = (SymGrpβπ·) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
7 | 4, 5, 6 | tocycf 32015 |
. . . . . . . . 9
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
8 | 1, 7 | syl 17 |
. . . . . . . 8
β’ (π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
9 | 8 | fdmd 6680 |
. . . . . . 7
β’ (π β dom π = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
10 | 3, 9 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
11 | 2, 10 | sselid 3943 |
. . . . 5
β’ (π β π β Word π·) |
12 | | pfxcl 14571 |
. . . . 5
β’ (π β Word π· β (π prefix πΈ) β Word π·) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β (π prefix πΈ) β Word π·) |
14 | | cycpmco2.i |
. . . . . 6
β’ (π β πΌ β (π· β ran π)) |
15 | 14 | eldifad 3923 |
. . . . 5
β’ (π β πΌ β π·) |
16 | 15 | s1cld 14497 |
. . . 4
β’ (π β β¨βπΌββ© β Word π·) |
17 | | ccatcl 14468 |
. . . 4
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
18 | 13, 16, 17 | syl2anc 585 |
. . 3
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
19 | | swrdcl 14539 |
. . . 4
β’ (π β Word π· β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
20 | 11, 19 | syl 17 |
. . 3
β’ (π β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
21 | | id 22 |
. . . . . . . . 9
β’ (π€ = π β π€ = π) |
22 | | dmeq 5860 |
. . . . . . . . 9
β’ (π€ = π β dom π€ = dom π) |
23 | | eqidd 2734 |
. . . . . . . . 9
β’ (π€ = π β π· = π·) |
24 | 21, 22, 23 | f1eq123d 6777 |
. . . . . . . 8
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
25 | 24 | elrab 3646 |
. . . . . . 7
β’ (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π β Word π· β§ π:dom πβ1-1βπ·)) |
26 | 10, 25 | sylib 217 |
. . . . . 6
β’ (π β (π β Word π· β§ π:dom πβ1-1βπ·)) |
27 | 26 | simprd 497 |
. . . . 5
β’ (π β π:dom πβ1-1βπ·) |
28 | | cycpmco2.e |
. . . . . 6
β’ πΈ = ((β‘πβπ½) + 1) |
29 | | f1cnv 6809 |
. . . . . . . . . 10
β’ (π:dom πβ1-1βπ· β β‘π:ran πβ1-1-ontoβdom
π) |
30 | | f1of 6785 |
. . . . . . . . . 10
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
31 | 27, 29, 30 | 3syl 18 |
. . . . . . . . 9
β’ (π β β‘π:ran πβΆdom π) |
32 | | cycpmco2.j |
. . . . . . . . 9
β’ (π β π½ β ran π) |
33 | 31, 32 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π β (β‘πβπ½) β dom π) |
34 | | wrddm 14415 |
. . . . . . . . 9
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
35 | 11, 34 | syl 17 |
. . . . . . . 8
β’ (π β dom π = (0..^(β―βπ))) |
36 | 33, 35 | eleqtrd 2836 |
. . . . . . 7
β’ (π β (β‘πβπ½) β (0..^(β―βπ))) |
37 | | fzofzp1 13675 |
. . . . . . 7
β’ ((β‘πβπ½) β (0..^(β―βπ)) β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
38 | 36, 37 | syl 17 |
. . . . . 6
β’ (π β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
39 | 28, 38 | eqeltrid 2838 |
. . . . 5
β’ (π β πΈ β (0...(β―βπ))) |
40 | 11, 27, 39 | pfxf1 31847 |
. . . 4
β’ (π β (π prefix πΈ):dom (π prefix πΈ)β1-1βπ·) |
41 | 15 | s1f1 31848 |
. . . 4
β’ (π β β¨βπΌββ©:dom
β¨βπΌββ©β1-1βπ·) |
42 | | s1rn 14493 |
. . . . . . 7
β’ (πΌ β π· β ran β¨βπΌββ© = {πΌ}) |
43 | 15, 42 | syl 17 |
. . . . . 6
β’ (π β ran β¨βπΌββ© = {πΌ}) |
44 | 43 | ineq2d 4173 |
. . . . 5
β’ (π β (ran (π prefix πΈ) β© ran β¨βπΌββ©) = (ran (π prefix πΈ) β© {πΌ})) |
45 | | pfxrn2 31845 |
. . . . . . . . 9
β’ ((π β Word π· β§ πΈ β (0...(β―βπ))) β ran (π prefix πΈ) β ran π) |
46 | 11, 39, 45 | syl2anc 585 |
. . . . . . . 8
β’ (π β ran (π prefix πΈ) β ran π) |
47 | 46 | ssrind 4196 |
. . . . . . 7
β’ (π β (ran (π prefix πΈ) β© {πΌ}) β (ran π β© {πΌ})) |
48 | 14 | eldifbd 3924 |
. . . . . . . 8
β’ (π β Β¬ πΌ β ran π) |
49 | | disjsn 4673 |
. . . . . . . 8
β’ ((ran
π β© {πΌ}) = β
β Β¬ πΌ β ran π) |
50 | 48, 49 | sylibr 233 |
. . . . . . 7
β’ (π β (ran π β© {πΌ}) = β
) |
51 | 47, 50 | sseqtrd 3985 |
. . . . . 6
β’ (π β (ran (π prefix πΈ) β© {πΌ}) β β
) |
52 | | ss0 4359 |
. . . . . 6
β’ ((ran
(π prefix πΈ) β© {πΌ}) β β
β (ran (π prefix πΈ) β© {πΌ}) = β
) |
53 | 51, 52 | syl 17 |
. . . . 5
β’ (π β (ran (π prefix πΈ) β© {πΌ}) = β
) |
54 | 44, 53 | eqtrd 2773 |
. . . 4
β’ (π β (ran (π prefix πΈ) β© ran β¨βπΌββ©) = β
) |
55 | 1, 13, 16, 40, 41, 54 | ccatf1 31854 |
. . 3
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©):dom ((π prefix πΈ) ++ β¨βπΌββ©)β1-1βπ·) |
56 | | lencl 14427 |
. . . . 5
β’ (π β Word π· β (β―βπ) β
β0) |
57 | | nn0fz0 13545 |
. . . . . 6
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
58 | 57 | biimpi 215 |
. . . . 5
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
59 | 11, 56, 58 | 3syl 18 |
. . . 4
β’ (π β (β―βπ) β
(0...(β―βπ))) |
60 | 11, 39, 59, 27 | swrdf1 31859 |
. . 3
β’ (π β (π substr β¨πΈ, (β―βπ)β©):dom (π substr β¨πΈ, (β―βπ)β©)β1-1βπ·) |
61 | | ccatrn 14483 |
. . . . . . 7
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ran ((π prefix πΈ) ++ β¨βπΌββ©) = (ran (π prefix πΈ) βͺ ran β¨βπΌββ©)) |
62 | 13, 16, 61 | syl2anc 585 |
. . . . . 6
β’ (π β ran ((π prefix πΈ) ++ β¨βπΌββ©) = (ran (π prefix πΈ) βͺ ran β¨βπΌββ©)) |
63 | 62 | ineq1d 4172 |
. . . . 5
β’ (π β (ran ((π prefix πΈ) ++ β¨βπΌββ©) β© ran (π substr β¨πΈ, (β―βπ)β©)) = ((ran (π prefix πΈ) βͺ ran β¨βπΌββ©) β© ran (π substr β¨πΈ, (β―βπ)β©))) |
64 | | indir 4236 |
. . . . 5
β’ ((ran
(π prefix πΈ) βͺ ran β¨βπΌββ©) β© ran (π substr β¨πΈ, (β―βπ)β©)) = ((ran (π prefix πΈ) β© ran (π substr β¨πΈ, (β―βπ)β©)) βͺ (ran β¨βπΌββ© β© ran (π substr β¨πΈ, (β―βπ)β©))) |
65 | 63, 64 | eqtrdi 2789 |
. . . 4
β’ (π β (ran ((π prefix πΈ) ++ β¨βπΌββ©) β© ran (π substr β¨πΈ, (β―βπ)β©)) = ((ran (π prefix πΈ) β© ran (π substr β¨πΈ, (β―βπ)β©)) βͺ (ran β¨βπΌββ© β© ran (π substr β¨πΈ, (β―βπ)β©)))) |
66 | | fz0ssnn0 13542 |
. . . . . . . . . 10
β’
(0...(β―βπ)) β
β0 |
67 | 66, 39 | sselid 3943 |
. . . . . . . . 9
β’ (π β πΈ β
β0) |
68 | | pfxval 14567 |
. . . . . . . . 9
β’ ((π β Word π· β§ πΈ β β0) β (π prefix πΈ) = (π substr β¨0, πΈβ©)) |
69 | 11, 67, 68 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π prefix πΈ) = (π substr β¨0, πΈβ©)) |
70 | 69 | rneqd 5894 |
. . . . . . 7
β’ (π β ran (π prefix πΈ) = ran (π substr β¨0, πΈβ©)) |
71 | 70 | ineq1d 4172 |
. . . . . 6
β’ (π β (ran (π prefix πΈ) β© ran (π substr β¨πΈ, (β―βπ)β©)) = (ran (π substr β¨0, πΈβ©) β© ran (π substr β¨πΈ, (β―βπ)β©))) |
72 | | 0elfz 13544 |
. . . . . . . 8
β’ (πΈ β β0
β 0 β (0...πΈ)) |
73 | 67, 72 | syl 17 |
. . . . . . 7
β’ (π β 0 β (0...πΈ)) |
74 | | elfzuz3 13444 |
. . . . . . . 8
β’ (πΈ β
(0...(β―βπ))
β (β―βπ)
β (β€β₯βπΈ)) |
75 | | eluzfz1 13454 |
. . . . . . . 8
β’
((β―βπ)
β (β€β₯βπΈ) β πΈ β (πΈ...(β―βπ))) |
76 | 39, 74, 75 | 3syl 18 |
. . . . . . 7
β’ (π β πΈ β (πΈ...(β―βπ))) |
77 | | eluzfz2 13455 |
. . . . . . . 8
β’
((β―βπ)
β (β€β₯βπΈ) β (β―βπ) β (πΈ...(β―βπ))) |
78 | 39, 74, 77 | 3syl 18 |
. . . . . . 7
β’ (π β (β―βπ) β (πΈ...(β―βπ))) |
79 | 11, 73, 39, 27, 76, 78 | swrdrndisj 31860 |
. . . . . 6
β’ (π β (ran (π substr β¨0, πΈβ©) β© ran (π substr β¨πΈ, (β―βπ)β©)) = β
) |
80 | 71, 79 | eqtrd 2773 |
. . . . 5
β’ (π β (ran (π prefix πΈ) β© ran (π substr β¨πΈ, (β―βπ)β©)) = β
) |
81 | | incom 4162 |
. . . . . 6
β’ (ran
β¨βπΌββ©
β© ran (π substr
β¨πΈ,
(β―βπ)β©)) =
(ran (π substr β¨πΈ, (β―βπ)β©) β© ran
β¨βπΌββ©) |
82 | 43 | ineq2d 4173 |
. . . . . . 7
β’ (π β (ran (π substr β¨πΈ, (β―βπ)β©) β© ran β¨βπΌββ©) = (ran (π substr β¨πΈ, (β―βπ)β©) β© {πΌ})) |
83 | | swrdrn2 31857 |
. . . . . . . . . . 11
β’ ((π β Word π· β§ πΈ β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β ran (π substr
β¨πΈ,
(β―βπ)β©)
β ran π) |
84 | 11, 39, 59, 83 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ran (π substr β¨πΈ, (β―βπ)β©) β ran π) |
85 | 84 | ssrind 4196 |
. . . . . . . . 9
β’ (π β (ran (π substr β¨πΈ, (β―βπ)β©) β© {πΌ}) β (ran π β© {πΌ})) |
86 | 85, 50 | sseqtrd 3985 |
. . . . . . . 8
β’ (π β (ran (π substr β¨πΈ, (β―βπ)β©) β© {πΌ}) β β
) |
87 | | ss0 4359 |
. . . . . . . 8
β’ ((ran
(π substr β¨πΈ, (β―βπ)β©) β© {πΌ}) β β
β (ran
(π substr β¨πΈ, (β―βπ)β©) β© {πΌ}) = β
) |
88 | 86, 87 | syl 17 |
. . . . . . 7
β’ (π β (ran (π substr β¨πΈ, (β―βπ)β©) β© {πΌ}) = β
) |
89 | 82, 88 | eqtrd 2773 |
. . . . . 6
β’ (π β (ran (π substr β¨πΈ, (β―βπ)β©) β© ran β¨βπΌββ©) =
β
) |
90 | 81, 89 | eqtrid 2785 |
. . . . 5
β’ (π β (ran β¨βπΌββ© β© ran (π substr β¨πΈ, (β―βπ)β©)) = β
) |
91 | 80, 90 | uneq12d 4125 |
. . . 4
β’ (π β ((ran (π prefix πΈ) β© ran (π substr β¨πΈ, (β―βπ)β©)) βͺ (ran β¨βπΌββ© β© ran (π substr β¨πΈ, (β―βπ)β©))) = (β
βͺ
β
)) |
92 | | unidm 4113 |
. . . . 5
β’ (β
βͺ β
) = β
|
93 | 92 | a1i 11 |
. . . 4
β’ (π β (β
βͺ β
) =
β
) |
94 | 65, 91, 93 | 3eqtrd 2777 |
. . 3
β’ (π β (ran ((π prefix πΈ) ++ β¨βπΌββ©) β© ran (π substr β¨πΈ, (β―βπ)β©)) = β
) |
95 | 1, 18, 20, 55, 60, 94 | ccatf1 31854 |
. 2
β’ (π β (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)):dom (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β1-1βπ·) |
96 | | cycpmco2.1 |
. . . 4
β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) |
97 | | ovexd 7393 |
. . . . . 6
β’ (π β ((β‘πβπ½) + 1) β V) |
98 | 28, 97 | eqeltrid 2838 |
. . . . 5
β’ (π β πΈ β V) |
99 | | splval 14645 |
. . . . 5
β’ ((π β dom π β§ (πΈ β V β§ πΈ β V β§ β¨βπΌββ© β Word π·)) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
100 | 3, 98, 98, 16, 99 | syl13anc 1373 |
. . . 4
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
101 | 96, 100 | eqtrid 2785 |
. . 3
β’ (π β π = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
102 | 101 | dmeqd 5862 |
. . 3
β’ (π β dom π = dom (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
103 | | eqidd 2734 |
. . 3
β’ (π β π· = π·) |
104 | 101, 102,
103 | f1eq123d 6777 |
. 2
β’ (π β (π:dom πβ1-1βπ· β (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)):dom (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β1-1βπ·)) |
105 | 95, 104 | mpbird 257 |
1
β’ (π β π:dom πβ1-1βπ·) |