Step | Hyp | Ref
| Expression |
1 | | cycpmco2lem.1 |
. . . . 5
β’ (π β πΎ β ran π) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ (β―βπ) = πΈ) β πΎ β ran π) |
3 | | cycpmco2.1 |
. . . . . . . . . . . . . . 15
β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) |
4 | | cycpmco2.w |
. . . . . . . . . . . . . . . 16
β’ (π β π β dom π) |
5 | | cycpmco2.e |
. . . . . . . . . . . . . . . . 17
β’ πΈ = ((β‘πβπ½) + 1) |
6 | | ovexd 7393 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β‘πβπ½) + 1) β V) |
7 | 5, 6 | eqeltrid 2838 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ β V) |
8 | | cycpmco2.i |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΌ β (π· β ran π)) |
9 | 8 | eldifad 3923 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π·) |
10 | 9 | s1cld 14497 |
. . . . . . . . . . . . . . . 16
β’ (π β β¨βπΌββ© β Word π·) |
11 | | splval 14645 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom π β§ (πΈ β V β§ πΈ β V β§ β¨βπΌββ© β Word π·)) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
12 | 4, 7, 7, 10, 11 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
13 | 3, 12 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π β π = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
14 | 13 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ) = (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)))) |
15 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . 17
β’ {π€ β Word π· β£ π€:dom π€β1-1βπ·} β Word π· |
16 | | cycpmco2.d |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β π) |
17 | | cycpmco2.c |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (toCycβπ·) |
18 | | cycpmco2.s |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (SymGrpβπ·) |
19 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(Baseβπ) =
(Baseβπ) |
20 | 17, 18, 19 | tocycf 32015 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
22 | 21 | fdmd 6680 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom π = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
23 | 4, 22 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
24 | 15, 23 | sselid 3943 |
. . . . . . . . . . . . . . . 16
β’ (π β π β Word π·) |
25 | | pfxcl 14571 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π· β (π prefix πΈ) β Word π·) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π prefix πΈ) β Word π·) |
27 | | ccatcl 14468 |
. . . . . . . . . . . . . . 15
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
28 | 26, 10, 27 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
29 | | swrdcl 14539 |
. . . . . . . . . . . . . . 15
β’ (π β Word π· β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
30 | 24, 29 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
31 | | ccatlen 14469 |
. . . . . . . . . . . . . 14
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π·) β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
32 | 28, 30, 31 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
33 | | ccatws1len 14514 |
. . . . . . . . . . . . . . . 16
β’ ((π prefix πΈ) β Word π· β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
35 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π β π€ = π) |
36 | | dmeq 5860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π β dom π€ = dom π) |
37 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π β π· = π·) |
38 | 35, 36, 37 | f1eq123d 6777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
39 | 38 | elrab 3646 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π β Word π· β§ π:dom πβ1-1βπ·)) |
40 | 23, 39 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β Word π· β§ π:dom πβ1-1βπ·)) |
41 | 40 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π:dom πβ1-1βπ·) |
42 | | f1cnv 6809 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:dom πβ1-1βπ· β β‘π:ran πβ1-1-ontoβdom
π) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β‘π:ran πβ1-1-ontoβdom
π) |
44 | | f1of 6785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β‘π:ran πβΆdom π) |
46 | | cycpmco2.j |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π½ β ran π) |
47 | 45, 46 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘πβπ½) β dom π) |
48 | | wrddm 14415 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
49 | 24, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom π = (0..^(β―βπ))) |
50 | 47, 49 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β‘πβπ½) β (0..^(β―βπ))) |
51 | | fzofzp1 13675 |
. . . . . . . . . . . . . . . . . . 19
β’ ((β‘πβπ½) β (0..^(β―βπ)) β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
53 | 5, 52 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΈ β (0...(β―βπ))) |
54 | | pfxlen 14577 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Word π· β§ πΈ β (0...(β―βπ))) β (β―β(π prefix πΈ)) = πΈ) |
55 | 24, 53, 54 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―β(π prefix πΈ)) = πΈ) |
56 | 55 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π β ((β―β(π prefix πΈ)) + 1) = (πΈ + 1)) |
57 | 34, 56 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = (πΈ + 1)) |
58 | | lencl 14427 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π· β (β―βπ) β
β0) |
59 | 24, 58 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―βπ) β
β0) |
60 | | nn0fz0 13545 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
61 | 59, 60 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β (β―βπ) β
(0...(β―βπ))) |
62 | | swrdlen 14541 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π· β§ πΈ β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β (β―β(π
substr β¨πΈ,
(β―βπ)β©)) =
((β―βπ) β
πΈ)) |
63 | 24, 53, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β (β―β(π substr β¨πΈ, (β―βπ)β©)) = ((β―βπ) β πΈ)) |
64 | 57, 63 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π β ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
65 | 14, 32, 64 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (β―βπ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
66 | | fz0ssnn0 13542 |
. . . . . . . . . . . . . . . . 17
β’
(0...(β―βπ)) β
β0 |
67 | 66, 53 | sselid 3943 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ β
β0) |
68 | 67 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ β β€) |
69 | 68 | peano2zd 12615 |
. . . . . . . . . . . . . 14
β’ (π β (πΈ + 1) β β€) |
70 | 69 | zcnd 12613 |
. . . . . . . . . . . . 13
β’ (π β (πΈ + 1) β β) |
71 | 59 | nn0cnd 12480 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ) β
β) |
72 | 67 | nn0cnd 12480 |
. . . . . . . . . . . . 13
β’ (π β πΈ β β) |
73 | 70, 71, 72 | addsubassd 11537 |
. . . . . . . . . . . 12
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
74 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
75 | 72, 74, 71 | addassd 11182 |
. . . . . . . . . . . . 13
β’ (π β ((πΈ + 1) + (β―βπ)) = (πΈ + (1 + (β―βπ)))) |
76 | 75 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
77 | 65, 73, 76 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (π β (β―βπ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
78 | 74, 71 | addcld 11179 |
. . . . . . . . . . . 12
β’ (π β (1 + (β―βπ)) β
β) |
79 | 72, 78 | pncan2d 11519 |
. . . . . . . . . . 11
β’ (π β ((πΈ + (1 + (β―βπ))) β πΈ) = (1 + (β―βπ))) |
80 | 74, 71 | addcomd 11362 |
. . . . . . . . . . 11
β’ (π β (1 + (β―βπ)) = ((β―βπ) + 1)) |
81 | 77, 79, 80 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β (β―βπ) = ((β―βπ) + 1)) |
82 | | oveq1 7365 |
. . . . . . . . . 10
β’
((β―βπ) =
πΈ β
((β―βπ) + 1) =
(πΈ + 1)) |
83 | 81, 82 | sylan9eq 2793 |
. . . . . . . . 9
β’ ((π β§ (β―βπ) = πΈ) β (β―βπ) = (πΈ + 1)) |
84 | 83 | oveq1d 7373 |
. . . . . . . 8
β’ ((π β§ (β―βπ) = πΈ) β ((β―βπ) β 1) = ((πΈ + 1) β 1)) |
85 | 72, 74 | pncand 11518 |
. . . . . . . . 9
β’ (π β ((πΈ + 1) β 1) = πΈ) |
86 | 85 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) = πΈ) β ((πΈ + 1) β 1) = πΈ) |
87 | 84, 86 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ (β―βπ) = πΈ) β ((β―βπ) β 1) = πΈ) |
88 | 87 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ (β―βπ) = πΈ) β (πβ((β―βπ) β 1)) = (πβπΈ)) |
89 | | cycpmco2lem5.1 |
. . . . . . . . 9
β’ (π β (β‘πβπΎ) = ((β―βπ) β 1)) |
90 | 89 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (πβ(β‘πβπΎ)) = (πβ((β―βπ) β 1))) |
91 | 17, 18, 16, 4, 8, 46, 5, 3 | cycpmco2f1 32022 |
. . . . . . . . . . 11
β’ (π β π:dom πβ1-1βπ·) |
92 | | f1f1orn 6796 |
. . . . . . . . . . 11
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
93 | 91, 92 | syl 17 |
. . . . . . . . . 10
β’ (π β π:dom πβ1-1-ontoβran
π) |
94 | | ssun1 4133 |
. . . . . . . . . . . 12
β’ ran π β (ran π βͺ {πΌ}) |
95 | 17, 18, 16, 4, 8, 46, 5, 3 | cycpmco2rn 32023 |
. . . . . . . . . . . 12
β’ (π β ran π = (ran π βͺ {πΌ})) |
96 | 94, 95 | sseqtrrid 3998 |
. . . . . . . . . . 11
β’ (π β ran π β ran π) |
97 | 96 | sselda 3945 |
. . . . . . . . . 10
β’ ((π β§ πΎ β ran π) β πΎ β ran π) |
98 | | f1ocnvfv2 7224 |
. . . . . . . . . 10
β’ ((π:dom πβ1-1-ontoβran
π β§ πΎ β ran π) β (πβ(β‘πβπΎ)) = πΎ) |
99 | 93, 97, 98 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ πΎ β ran π) β (πβ(β‘πβπΎ)) = πΎ) |
100 | 1, 99 | mpdan 686 |
. . . . . . . 8
β’ (π β (πβ(β‘πβπΎ)) = πΎ) |
101 | 90, 100 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (πβ((β―βπ) β 1)) = πΎ) |
102 | 101 | adantr 482 |
. . . . . 6
β’ ((π β§ (β―βπ) = πΈ) β (πβ((β―βπ) β 1)) = πΎ) |
103 | 17, 18, 16, 4, 8, 46, 5, 3 | cycpmco2lem2 32025 |
. . . . . . 7
β’ (π β (πβπΈ) = πΌ) |
104 | 103 | adantr 482 |
. . . . . 6
β’ ((π β§ (β―βπ) = πΈ) β (πβπΈ) = πΌ) |
105 | 88, 102, 104 | 3eqtr3d 2781 |
. . . . 5
β’ ((π β§ (β―βπ) = πΈ) β πΎ = πΌ) |
106 | 8 | eldifbd 3924 |
. . . . . 6
β’ (π β Β¬ πΌ β ran π) |
107 | 106 | adantr 482 |
. . . . 5
β’ ((π β§ (β―βπ) = πΈ) β Β¬ πΌ β ran π) |
108 | 105, 107 | eqneltrd 2854 |
. . . 4
β’ ((π β§ (β―βπ) = πΈ) β Β¬ πΎ β ran π) |
109 | 2, 108 | pm2.21dd 194 |
. . 3
β’ ((π β§ (β―βπ) = πΈ) β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)β(πβ((β―βπ) β 1)))) |
110 | | splcl 14646 |
. . . . . . . 8
β’ ((π β Word π· β§ β¨βπΌββ© β Word π·) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
111 | 24, 10, 110 | syl2anc 585 |
. . . . . . 7
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
112 | 3, 111 | eqeltrid 2838 |
. . . . . 6
β’ (π β π β Word π·) |
113 | | nn0p1gt0 12447 |
. . . . . . . 8
β’
((β―βπ)
β β0 β 0 < ((β―βπ) + 1)) |
114 | 59, 113 | syl 17 |
. . . . . . 7
β’ (π β 0 <
((β―βπ) +
1)) |
115 | 114, 81 | breqtrrd 5134 |
. . . . . 6
β’ (π β 0 <
(β―βπ)) |
116 | | eqidd 2734 |
. . . . . 6
β’ (π β ((β―βπ) β 1) =
((β―βπ) β
1)) |
117 | 17, 16, 112, 91, 115, 116 | cycpmfv2 32012 |
. . . . 5
β’ (π β ((πβπ)β(πβ((β―βπ) β 1))) = (πβ0)) |
118 | 117 | adantr 482 |
. . . 4
β’ ((π β§ (β―βπ) β πΈ) β ((πβπ)β(πβ((β―βπ) β 1))) = (πβ0)) |
119 | | f1f 6739 |
. . . . . . . . . . . 12
β’ (π:dom πβ1-1βπ· β π:dom πβΆπ·) |
120 | 41, 119 | syl 17 |
. . . . . . . . . . 11
β’ (π β π:dom πβΆπ·) |
121 | 120 | frnd 6677 |
. . . . . . . . . 10
β’ (π β ran π β π·) |
122 | 16, 121 | ssexd 5282 |
. . . . . . . . 9
β’ (π β ran π β V) |
123 | 46 | ne0d 4296 |
. . . . . . . . 9
β’ (π β ran π β β
) |
124 | | hashgt0 14294 |
. . . . . . . . 9
β’ ((ran
π β V β§ ran π β β
) β 0 <
(β―βran π)) |
125 | 122, 123,
124 | syl2anc 585 |
. . . . . . . 8
β’ (π β 0 < (β―βran
π)) |
126 | 4 | dmexd 7843 |
. . . . . . . . 9
β’ (π β dom π β V) |
127 | | hashf1rn 14258 |
. . . . . . . . 9
β’ ((dom
π β V β§ π:dom πβ1-1βπ·) β (β―βπ) = (β―βran π)) |
128 | 126, 41, 127 | syl2anc 585 |
. . . . . . . 8
β’ (π β (β―βπ) = (β―βran π)) |
129 | 125, 128 | breqtrrd 5134 |
. . . . . . 7
β’ (π β 0 <
(β―βπ)) |
130 | | eqidd 2734 |
. . . . . . 7
β’ (π β ((β―βπ) β 1) =
((β―βπ) β
1)) |
131 | 17, 16, 24, 41, 129, 130 | cycpmfv2 32012 |
. . . . . 6
β’ (π β ((πβπ)β(πβ((β―βπ) β 1))) = (πβ0)) |
132 | 131 | adantr 482 |
. . . . 5
β’ ((π β§ (β―βπ) β πΈ) β ((πβπ)β(πβ((β―βπ) β 1))) = (πβ0)) |
133 | 3 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©)) |
134 | 17, 18, 16, 4, 8, 46, 5, 3 | cycpmco2lem3 32026 |
. . . . . . . . . 10
β’ (π β ((β―βπ) β 1) =
(β―βπ)) |
135 | 72, 74 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (π β (πΈ + 1) = (1 + πΈ)) |
136 | 135 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β ((((β―βπ) β 1) β πΈ) + (πΈ + 1)) = ((((β―βπ) β 1) β πΈ) + (1 + πΈ))) |
137 | 71, 74 | subcld 11517 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ) β 1) β
β) |
138 | 137, 72, 74 | nppcan3d 11544 |
. . . . . . . . . . 11
β’ (π β ((((β―βπ) β 1) β πΈ) + (1 + πΈ)) = (((β―βπ) β 1) + 1)) |
139 | 71, 74 | npcand 11521 |
. . . . . . . . . . 11
β’ (π β (((β―βπ) β 1) + 1) =
(β―βπ)) |
140 | 136, 138,
139 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β ((((β―βπ) β 1) β πΈ) + (πΈ + 1)) = (β―βπ)) |
141 | 134, 140 | eqtr4d 2776 |
. . . . . . . . 9
β’ (π β ((β―βπ) β 1) =
((((β―βπ)
β 1) β πΈ) +
(πΈ + 1))) |
142 | 141 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β ((β―βπ) β 1) = ((((β―βπ) β 1) β πΈ) + (πΈ + 1))) |
143 | 133, 142 | fveq12d 6850 |
. . . . . . 7
β’ ((π β§ (β―βπ) β πΈ) β (πβ((β―βπ) β 1)) = ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β((((β―βπ) β 1) β πΈ) + (πΈ + 1)))) |
144 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β π β Word π·) |
145 | | nn0fz0 13545 |
. . . . . . . . . 10
β’ (πΈ β β0
β πΈ β (0...πΈ)) |
146 | 67, 145 | sylib 217 |
. . . . . . . . 9
β’ (π β πΈ β (0...πΈ)) |
147 | 146 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β πΈ β (0...πΈ)) |
148 | 53 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β πΈ β (0...(β―βπ))) |
149 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β β¨βπΌββ© β Word π·) |
150 | 71 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (β―βπ) β πΈ) β (β―βπ) β β) |
151 | | 1cnd 11155 |
. . . . . . . . . 10
β’ ((π β§ (β―βπ) β πΈ) β 1 β β) |
152 | 72 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (β―βπ) β πΈ) β πΈ β β) |
153 | 150, 151,
152 | sub32d 11549 |
. . . . . . . . 9
β’ ((π β§ (β―βπ) β πΈ) β (((β―βπ) β 1) β πΈ) = (((β―βπ) β πΈ) β 1)) |
154 | | fznn0sub 13479 |
. . . . . . . . . . . . 13
β’ (πΈ β
(0...(β―βπ))
β ((β―βπ)
β πΈ) β
β0) |
155 | 53, 154 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ) β πΈ) β
β0) |
156 | 155 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (β―βπ) β πΈ) β ((β―βπ) β πΈ) β
β0) |
157 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ (β―βπ) β πΈ) β (β―βπ) β πΈ) |
158 | 150, 152,
156, 157 | subne0nn 31766 |
. . . . . . . . . 10
β’ ((π β§ (β―βπ) β πΈ) β ((β―βπ) β πΈ) β β) |
159 | | fzo0end 13670 |
. . . . . . . . . 10
β’
(((β―βπ)
β πΈ) β β
β (((β―βπ)
β πΈ) β 1)
β (0..^((β―βπ) β πΈ))) |
160 | 158, 159 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (β―βπ) β πΈ) β (((β―βπ) β πΈ) β 1) β
(0..^((β―βπ)
β πΈ))) |
161 | 153, 160 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β (((β―βπ) β 1) β πΈ) β (0..^((β―βπ) β πΈ))) |
162 | | s1len 14500 |
. . . . . . . . . . 11
β’
(β―ββ¨βπΌββ©) = 1 |
163 | 162 | eqcomi 2742 |
. . . . . . . . . 10
β’ 1 =
(β―ββ¨βπΌββ©) |
164 | 163 | oveq2i 7369 |
. . . . . . . . 9
β’ (πΈ + 1) = (πΈ + (β―ββ¨βπΌββ©)) |
165 | 164 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (β―βπ) β πΈ) β (πΈ + 1) = (πΈ + (β―ββ¨βπΌββ©))) |
166 | 144, 147,
148, 149, 161, 165 | splfv3 31861 |
. . . . . . 7
β’ ((π β§ (β―βπ) β πΈ) β ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β((((β―βπ) β 1) β πΈ) + (πΈ + 1))) = (πβ((((β―βπ) β 1) β πΈ) + πΈ))) |
167 | 137, 72 | npcand 11521 |
. . . . . . . . 9
β’ (π β ((((β―βπ) β 1) β πΈ) + πΈ) = ((β―βπ) β 1)) |
168 | 167 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (πβ((((β―βπ) β 1) β πΈ) + πΈ)) = (πβ((β―βπ) β 1))) |
169 | 168 | adantr 482 |
. . . . . . 7
β’ ((π β§ (β―βπ) β πΈ) β (πβ((((β―βπ) β 1) β πΈ) + πΈ)) = (πβ((β―βπ) β 1))) |
170 | 143, 166,
169 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β§ (β―βπ) β πΈ) β (πβ((β―βπ) β 1)) = (πβ((β―βπ) β 1))) |
171 | 170 | fveq2d 6847 |
. . . . 5
β’ ((π β§ (β―βπ) β πΈ) β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)β(πβ((β―βπ) β 1)))) |
172 | 13 | fveq1d 6845 |
. . . . . . 7
β’ (π β (πβ0) = ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0)) |
173 | | nn0p1nn 12457 |
. . . . . . . . . . . 12
β’ (πΈ β β0
β (πΈ + 1) β
β) |
174 | 67, 173 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΈ + 1) β β) |
175 | | lbfzo0 13618 |
. . . . . . . . . . 11
β’ (0 β
(0..^(πΈ + 1)) β (πΈ + 1) β
β) |
176 | 174, 175 | sylibr 233 |
. . . . . . . . . 10
β’ (π β 0 β (0..^(πΈ + 1))) |
177 | 57 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β
(0..^(β―β((π
prefix πΈ) ++
β¨βπΌββ©))) = (0..^(πΈ + 1))) |
178 | 176, 177 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β 0 β
(0..^(β―β((π
prefix πΈ) ++
β¨βπΌββ©)))) |
179 | | ccatval1 14471 |
. . . . . . . . 9
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π· β§ 0 β (0..^(β―β((π prefix πΈ) ++ β¨βπΌββ©)))) β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (((π prefix πΈ) ++ β¨βπΌββ©)β0)) |
180 | 28, 30, 178, 179 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (((π prefix πΈ) ++ β¨βπΌββ©)β0)) |
181 | | elfzonn0 13623 |
. . . . . . . . . . . . . 14
β’ ((β‘πβπ½) β (0..^(β―βπ)) β (β‘πβπ½) β
β0) |
182 | 50, 181 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β‘πβπ½) β
β0) |
183 | | nn0p1nn 12457 |
. . . . . . . . . . . . 13
β’ ((β‘πβπ½) β β0 β ((β‘πβπ½) + 1) β β) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β‘πβπ½) + 1) β β) |
185 | 5, 184 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β πΈ β β) |
186 | | lbfzo0 13618 |
. . . . . . . . . . 11
β’ (0 β
(0..^πΈ) β πΈ β
β) |
187 | 185, 186 | sylibr 233 |
. . . . . . . . . 10
β’ (π β 0 β (0..^πΈ)) |
188 | 55 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β (0..^(β―β(π prefix πΈ))) = (0..^πΈ)) |
189 | 187, 188 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β 0 β
(0..^(β―β(π
prefix πΈ)))) |
190 | | ccatval1 14471 |
. . . . . . . . 9
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π· β§ 0 β (0..^(β―β(π prefix πΈ)))) β (((π prefix πΈ) ++ β¨βπΌββ©)β0) = ((π prefix πΈ)β0)) |
191 | 26, 10, 189, 190 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((π prefix πΈ) ++ β¨βπΌββ©)β0) = ((π prefix πΈ)β0)) |
192 | | nn0p1gt0 12447 |
. . . . . . . . . . . . . 14
β’ ((β‘πβπ½) β β0 β 0 <
((β‘πβπ½) + 1)) |
193 | 182, 192 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((β‘πβπ½) + 1)) |
194 | 193, 5 | breqtrrdi 5148 |
. . . . . . . . . . . 12
β’ (π β 0 < πΈ) |
195 | 194 | gt0ne0d 11724 |
. . . . . . . . . . 11
β’ (π β πΈ β 0) |
196 | | fzne1 31738 |
. . . . . . . . . . 11
β’ ((πΈ β
(0...(β―βπ))
β§ πΈ β 0) β
πΈ β ((0 +
1)...(β―βπ))) |
197 | 53, 195, 196 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β πΈ β ((0 + 1)...(β―βπ))) |
198 | | 0p1e1 12280 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
199 | 198 | oveq1i 7368 |
. . . . . . . . . 10
β’ ((0 +
1)...(β―βπ)) =
(1...(β―βπ)) |
200 | 197, 199 | eleqtrdi 2844 |
. . . . . . . . 9
β’ (π β πΈ β (1...(β―βπ))) |
201 | | pfxfv0 14586 |
. . . . . . . . 9
β’ ((π β Word π· β§ πΈ β (1...(β―βπ))) β ((π prefix πΈ)β0) = (πβ0)) |
202 | 24, 200, 201 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π prefix πΈ)β0) = (πβ0)) |
203 | 180, 191,
202 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (πβ0)) |
204 | 172, 203 | eqtrd 2773 |
. . . . . 6
β’ (π β (πβ0) = (πβ0)) |
205 | 204 | adantr 482 |
. . . . 5
β’ ((π β§ (β―βπ) β πΈ) β (πβ0) = (πβ0)) |
206 | 132, 171,
205 | 3eqtr4rd 2784 |
. . . 4
β’ ((π β§ (β―βπ) β πΈ) β (πβ0) = ((πβπ)β(πβ((β―βπ) β 1)))) |
207 | 118, 206 | eqtrd 2773 |
. . 3
β’ ((π β§ (β―βπ) β πΈ) β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)β(πβ((β―βπ) β 1)))) |
208 | 109, 207 | pm2.61dane 3029 |
. 2
β’ (π β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)β(πβ((β―βπ) β 1)))) |
209 | 101 | fveq2d 6847 |
. 2
β’ (π β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)βπΎ)) |
210 | 101 | fveq2d 6847 |
. 2
β’ (π β ((πβπ)β(πβ((β―βπ) β 1))) = ((πβπ)βπΎ)) |
211 | 208, 209,
210 | 3eqtr3d 2781 |
1
β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) |