Step | Hyp | Ref
| Expression |
1 | | un23 4129 |
. 2
β’ (((π β (0..^πΈ)) βͺ {πΌ}) βͺ (π β (πΈ..^(β―βπ)))) = (((π β (0..^πΈ)) βͺ (π β (πΈ..^(β―βπ)))) βͺ {πΌ}) |
2 | | cycpmco2.1 |
. . . . 5
β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) |
3 | | cycpmco2.w |
. . . . . 6
β’ (π β π β dom π) |
4 | | cycpmco2.e |
. . . . . . 7
β’ πΈ = ((β‘πβπ½) + 1) |
5 | | ovexd 7393 |
. . . . . . 7
β’ (π β ((β‘πβπ½) + 1) β V) |
6 | 4, 5 | eqeltrid 2838 |
. . . . . 6
β’ (π β πΈ β V) |
7 | | cycpmco2.i |
. . . . . . . 8
β’ (π β πΌ β (π· β ran π)) |
8 | 7 | eldifad 3923 |
. . . . . . 7
β’ (π β πΌ β π·) |
9 | 8 | s1cld 14497 |
. . . . . 6
β’ (π β β¨βπΌββ© β Word π·) |
10 | | splval 14645 |
. . . . . 6
β’ ((π β dom π β§ (πΈ β V β§ πΈ β V β§ β¨βπΌββ© β Word π·)) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
11 | 3, 6, 6, 9, 10 | syl13anc 1373 |
. . . . 5
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
12 | 2, 11 | eqtrid 2785 |
. . . 4
β’ (π β π = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
13 | 12 | rneqd 5894 |
. . 3
β’ (π β ran π = ran (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
14 | | ssrab2 4038 |
. . . . . . 7
β’ {π€ β Word π· β£ π€:dom π€β1-1βπ·} β Word π· |
15 | | cycpmco2.d |
. . . . . . . . . 10
β’ (π β π· β π) |
16 | | cycpmco2.c |
. . . . . . . . . . 11
β’ π = (toCycβπ·) |
17 | | cycpmco2.s |
. . . . . . . . . . 11
β’ π = (SymGrpβπ·) |
18 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
19 | 16, 17, 18 | tocycf 32015 |
. . . . . . . . . 10
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
20 | 15, 19 | syl 17 |
. . . . . . . . 9
β’ (π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
21 | 20 | fdmd 6680 |
. . . . . . . 8
β’ (π β dom π = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
22 | 3, 21 | eleqtrd 2836 |
. . . . . . 7
β’ (π β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
23 | 14, 22 | sselid 3943 |
. . . . . 6
β’ (π β π β Word π·) |
24 | | pfxcl 14571 |
. . . . . 6
β’ (π β Word π· β (π prefix πΈ) β Word π·) |
25 | 23, 24 | syl 17 |
. . . . 5
β’ (π β (π prefix πΈ) β Word π·) |
26 | | ccatcl 14468 |
. . . . 5
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
27 | 25, 9, 26 | syl2anc 585 |
. . . 4
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
28 | | swrdcl 14539 |
. . . . 5
β’ (π β Word π· β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
29 | 23, 28 | syl 17 |
. . . 4
β’ (π β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
30 | | ccatrn 14483 |
. . . 4
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π·) β ran (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)) = (ran ((π prefix πΈ) ++ β¨βπΌββ©) βͺ ran (π substr β¨πΈ, (β―βπ)β©))) |
31 | 27, 29, 30 | syl2anc 585 |
. . 3
β’ (π β ran (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)) = (ran ((π prefix πΈ) ++ β¨βπΌββ©) βͺ ran (π substr β¨πΈ, (β―βπ)β©))) |
32 | | ccatrn 14483 |
. . . . . 6
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ran ((π prefix πΈ) ++ β¨βπΌββ©) = (ran (π prefix πΈ) βͺ ran β¨βπΌββ©)) |
33 | 25, 9, 32 | syl2anc 585 |
. . . . 5
β’ (π β ran ((π prefix πΈ) ++ β¨βπΌββ©) = (ran (π prefix πΈ) βͺ ran β¨βπΌββ©)) |
34 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β π€ = π) |
35 | | dmeq 5860 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β dom π€ = dom π) |
36 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β π· = π·) |
37 | 34, 35, 36 | f1eq123d 6777 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
38 | 37 | elrab 3646 |
. . . . . . . . . . . . . 14
β’ (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π β Word π· β§ π:dom πβ1-1βπ·)) |
39 | 22, 38 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β (π β Word π· β§ π:dom πβ1-1βπ·)) |
40 | 39 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β π:dom πβ1-1βπ·) |
41 | | f1cnv 6809 |
. . . . . . . . . . . 12
β’ (π:dom πβ1-1βπ· β β‘π:ran πβ1-1-ontoβdom
π) |
42 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β β‘π:ran πβΆdom π) |
44 | | cycpmco2.j |
. . . . . . . . . . 11
β’ (π β π½ β ran π) |
45 | 43, 44 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (π β (β‘πβπ½) β dom π) |
46 | | wrddm 14415 |
. . . . . . . . . . 11
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
47 | 23, 46 | syl 17 |
. . . . . . . . . 10
β’ (π β dom π = (0..^(β―βπ))) |
48 | 45, 47 | eleqtrd 2836 |
. . . . . . . . 9
β’ (π β (β‘πβπ½) β (0..^(β―βπ))) |
49 | | fzofzp1 13675 |
. . . . . . . . 9
β’ ((β‘πβπ½) β (0..^(β―βπ)) β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
β’ (π β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
51 | 4, 50 | eqeltrid 2838 |
. . . . . . 7
β’ (π β πΈ β (0...(β―βπ))) |
52 | | pfxrn3 31846 |
. . . . . . 7
β’ ((π β Word π· β§ πΈ β (0...(β―βπ))) β ran (π prefix πΈ) = (π β (0..^πΈ))) |
53 | 23, 51, 52 | syl2anc 585 |
. . . . . 6
β’ (π β ran (π prefix πΈ) = (π β (0..^πΈ))) |
54 | | s1rn 14493 |
. . . . . . 7
β’ (πΌ β π· β ran β¨βπΌββ© = {πΌ}) |
55 | 8, 54 | syl 17 |
. . . . . 6
β’ (π β ran β¨βπΌββ© = {πΌ}) |
56 | 53, 55 | uneq12d 4125 |
. . . . 5
β’ (π β (ran (π prefix πΈ) βͺ ran β¨βπΌββ©) = ((π β (0..^πΈ)) βͺ {πΌ})) |
57 | 33, 56 | eqtrd 2773 |
. . . 4
β’ (π β ran ((π prefix πΈ) ++ β¨βπΌββ©) = ((π β (0..^πΈ)) βͺ {πΌ})) |
58 | | lencl 14427 |
. . . . . 6
β’ (π β Word π· β (β―βπ) β
β0) |
59 | | nn0fz0 13545 |
. . . . . . 7
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
60 | 59 | biimpi 215 |
. . . . . 6
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
61 | 23, 58, 60 | 3syl 18 |
. . . . 5
β’ (π β (β―βπ) β
(0...(β―βπ))) |
62 | | swrdrn3 31858 |
. . . . 5
β’ ((π β Word π· β§ πΈ β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β ran (π substr
β¨πΈ,
(β―βπ)β©) =
(π β (πΈ..^(β―βπ)))) |
63 | 23, 51, 61, 62 | syl3anc 1372 |
. . . 4
β’ (π β ran (π substr β¨πΈ, (β―βπ)β©) = (π β (πΈ..^(β―βπ)))) |
64 | 57, 63 | uneq12d 4125 |
. . 3
β’ (π β (ran ((π prefix πΈ) ++ β¨βπΌββ©) βͺ ran (π substr β¨πΈ, (β―βπ)β©)) = (((π β (0..^πΈ)) βͺ {πΌ}) βͺ (π β (πΈ..^(β―βπ))))) |
65 | 13, 31, 64 | 3eqtrd 2777 |
. 2
β’ (π β ran π = (((π β (0..^πΈ)) βͺ {πΌ}) βͺ (π β (πΈ..^(β―βπ))))) |
66 | | fzosplit 13611 |
. . . . . 6
β’ (πΈ β
(0...(β―βπ))
β (0..^(β―βπ)) = ((0..^πΈ) βͺ (πΈ..^(β―βπ)))) |
67 | 51, 66 | syl 17 |
. . . . 5
β’ (π β (0..^(β―βπ)) = ((0..^πΈ) βͺ (πΈ..^(β―βπ)))) |
68 | 67 | imaeq2d 6014 |
. . . 4
β’ (π β (π β (0..^(β―βπ))) = (π β ((0..^πΈ) βͺ (πΈ..^(β―βπ))))) |
69 | | wrdf 14413 |
. . . . . . 7
β’ (π β Word π· β π:(0..^(β―βπ))βΆπ·) |
70 | 23, 69 | syl 17 |
. . . . . 6
β’ (π β π:(0..^(β―βπ))βΆπ·) |
71 | 70 | ffnd 6670 |
. . . . 5
β’ (π β π Fn (0..^(β―βπ))) |
72 | | fnima 6632 |
. . . . 5
β’ (π Fn (0..^(β―βπ)) β (π β (0..^(β―βπ))) = ran π) |
73 | 71, 72 | syl 17 |
. . . 4
β’ (π β (π β (0..^(β―βπ))) = ran π) |
74 | | elfzuz3 13444 |
. . . . . 6
β’ (πΈ β
(0...(β―βπ))
β (β―βπ)
β (β€β₯βπΈ)) |
75 | | fzoss2 13606 |
. . . . . 6
β’
((β―βπ)
β (β€β₯βπΈ) β (0..^πΈ) β (0..^(β―βπ))) |
76 | 51, 74, 75 | 3syl 18 |
. . . . 5
β’ (π β (0..^πΈ) β (0..^(β―βπ))) |
77 | | fz0ssnn0 13542 |
. . . . . . . 8
β’
(0...(β―βπ)) β
β0 |
78 | 77, 51 | sselid 3943 |
. . . . . . 7
β’ (π β πΈ β
β0) |
79 | | nn0uz 12810 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
80 | 78, 79 | eleqtrdi 2844 |
. . . . . 6
β’ (π β πΈ β
(β€β₯β0)) |
81 | | fzoss1 13605 |
. . . . . 6
β’ (πΈ β
(β€β₯β0) β (πΈ..^(β―βπ)) β (0..^(β―βπ))) |
82 | 80, 81 | syl 17 |
. . . . 5
β’ (π β (πΈ..^(β―βπ)) β (0..^(β―βπ))) |
83 | | unima 6917 |
. . . . 5
β’ ((π Fn (0..^(β―βπ)) β§ (0..^πΈ) β (0..^(β―βπ)) β§ (πΈ..^(β―βπ)) β (0..^(β―βπ))) β (π β ((0..^πΈ) βͺ (πΈ..^(β―βπ)))) = ((π β (0..^πΈ)) βͺ (π β (πΈ..^(β―βπ))))) |
84 | 71, 76, 82, 83 | syl3anc 1372 |
. . . 4
β’ (π β (π β ((0..^πΈ) βͺ (πΈ..^(β―βπ)))) = ((π β (0..^πΈ)) βͺ (π β (πΈ..^(β―βπ))))) |
85 | 68, 73, 84 | 3eqtr3d 2781 |
. . 3
β’ (π β ran π = ((π β (0..^πΈ)) βͺ (π β (πΈ..^(β―βπ))))) |
86 | 85 | uneq1d 4123 |
. 2
β’ (π β (ran π βͺ {πΌ}) = (((π β (0..^πΈ)) βͺ (π β (πΈ..^(β―βπ)))) βͺ {πΌ})) |
87 | 1, 65, 86 | 3eqtr4a 2799 |
1
β’ (π β ran π = (ran π βͺ {πΌ})) |