Step | Hyp | Ref
| Expression |
1 | | cycpmco2.c |
. . 3
β’ π = (toCycβπ·) |
2 | | cycpmco2.s |
. . 3
β’ π = (SymGrpβπ·) |
3 | | cycpmco2.d |
. . 3
β’ (π β π· β π) |
4 | | cycpmco2.w |
. . 3
β’ (π β π β dom π) |
5 | | cycpmco2.i |
. . 3
β’ (π β πΌ β (π· β ran π)) |
6 | | cycpmco2.j |
. . 3
β’ (π β π½ β ran π) |
7 | | cycpmco2.e |
. . 3
β’ πΈ = ((β‘πβπ½) + 1) |
8 | | cycpmco2.1 |
. . 3
β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem1 32024 |
. 2
β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπ½)) |
10 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β π· β π) |
11 | | ssrab2 4038 |
. . . . . . . . 9
β’ {π€ β Word π· β£ π€:dom π€β1-1βπ·} β Word π· |
12 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
13 | 1, 2, 12 | tocycf 32015 |
. . . . . . . . . . . 12
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . 11
β’ (π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
15 | 14 | fdmd 6680 |
. . . . . . . . . 10
β’ (π β dom π = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
16 | 4, 15 | eleqtrd 2836 |
. . . . . . . . 9
β’ (π β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
17 | 11, 16 | sselid 3943 |
. . . . . . . 8
β’ (π β π β Word π·) |
18 | 5 | eldifad 3923 |
. . . . . . . . 9
β’ (π β πΌ β π·) |
19 | 18 | s1cld 14497 |
. . . . . . . 8
β’ (π β β¨βπΌββ© β Word π·) |
20 | | splcl 14646 |
. . . . . . . 8
β’ ((π β Word π· β§ β¨βπΌββ© β Word π·) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
21 | 17, 19, 20 | syl2anc 585 |
. . . . . . 7
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
22 | 8, 21 | eqeltrid 2838 |
. . . . . 6
β’ (π β π β Word π·) |
23 | 22 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β π β Word π·) |
24 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2f1 32022 |
. . . . . 6
β’ (π β π:dom πβ1-1βπ·) |
25 | 24 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β π:dom πβ1-1βπ·) |
26 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β πΈ β (0..^(β―βπ))) |
27 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem3 32026 |
. . . . . . . 8
β’ (π β ((β―βπ) β 1) =
(β―βπ)) |
28 | 27 | oveq2d 7374 |
. . . . . . 7
β’ (π β (0..^((β―βπ) β 1)) =
(0..^(β―βπ))) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β
(0..^((β―βπ)
β 1)) = (0..^(β―βπ))) |
30 | 26, 29 | eleqtrrd 2837 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β πΈ β (0..^((β―βπ) β 1))) |
31 | 1, 10, 23, 25, 30 | cycpmfv1 32011 |
. . . 4
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)β(πβπΈ)) = (πβ(πΈ + 1))) |
32 | 1, 2, 3, 4, 5, 6, 7, 8 | cycpmco2lem2 32025 |
. . . . . 6
β’ (π β (πβπΈ) = πΌ) |
33 | 32 | fveq2d 6847 |
. . . . 5
β’ (π β ((πβπ)β(πβπΈ)) = ((πβπ)βπΌ)) |
34 | 33 | adantr 482 |
. . . 4
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)β(πβπΈ)) = ((πβπ)βπΌ)) |
35 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β π β Word π·) |
36 | | lencl 14427 |
. . . . . . . . 9
β’ (π β Word π· β (β―βπ) β
β0) |
37 | 17, 36 | syl 17 |
. . . . . . . 8
β’ (π β (β―βπ) β
β0) |
38 | | nn0fz0 13545 |
. . . . . . . 8
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
β’ (π β (β―βπ) β
(0...(β―βπ))) |
40 | 39 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β (β―βπ) β
(0...(β―βπ))) |
41 | | swrdfv0 14543 |
. . . . . 6
β’ ((π β Word π· β§ πΈ β (0..^(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β ((π substr
β¨πΈ,
(β―βπ)β©)β0) = (πβπΈ)) |
42 | 35, 26, 40, 41 | syl3anc 1372 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((π substr β¨πΈ, (β―βπ)β©)β0) = (πβπΈ)) |
43 | | ovexd 7393 |
. . . . . . . . . . 11
β’ (π β ((β‘πβπ½) + 1) β V) |
44 | 7, 43 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β πΈ β V) |
45 | | splval 14645 |
. . . . . . . . . 10
β’ ((π β dom π β§ (πΈ β V β§ πΈ β V β§ β¨βπΌββ© β Word π·)) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
46 | 4, 44, 44, 19, 45 | syl13anc 1373 |
. . . . . . . . 9
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
47 | 8, 46 | eqtrid 2785 |
. . . . . . . 8
β’ (π β π = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
48 | 47 | fveq1d 6845 |
. . . . . . 7
β’ (π β (πβ(πΈ + 1)) = ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β(πΈ + 1))) |
49 | 48 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πβ(πΈ + 1)) = ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β(πΈ + 1))) |
50 | | pfxcl 14571 |
. . . . . . . . . 10
β’ (π β Word π· β (π prefix πΈ) β Word π·) |
51 | 17, 50 | syl 17 |
. . . . . . . . 9
β’ (π β (π prefix πΈ) β Word π·) |
52 | | ccatcl 14468 |
. . . . . . . . 9
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
53 | 51, 19, 52 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
54 | 53 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
55 | | swrdcl 14539 |
. . . . . . . . 9
β’ (π β Word π· β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
56 | 17, 55 | syl 17 |
. . . . . . . 8
β’ (π β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
57 | 56 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β (0..^(β―βπ))) β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
58 | | 1z 12538 |
. . . . . . . . . . 11
β’ 1 β
β€ |
59 | | fzoaddel 13631 |
. . . . . . . . . . 11
β’ ((πΈ β
(0..^(β―βπ))
β§ 1 β β€) β (πΈ + 1) β ((0 +
1)..^((β―βπ) +
1))) |
60 | 58, 59 | mpan2 690 |
. . . . . . . . . 10
β’ (πΈ β
(0..^(β―βπ))
β (πΈ + 1) β ((0 +
1)..^((β―βπ) +
1))) |
61 | | elfzolt2b 13589 |
. . . . . . . . . 10
β’ ((πΈ + 1) β ((0 +
1)..^((β―βπ) +
1)) β (πΈ + 1) β
((πΈ +
1)..^((β―βπ) +
1))) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
β’ (πΈ β
(0..^(β―βπ))
β (πΈ + 1) β
((πΈ +
1)..^((β―βπ) +
1))) |
63 | 62 | adantl 483 |
. . . . . . . 8
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πΈ + 1) β ((πΈ + 1)..^((β―βπ) + 1))) |
64 | | ccatws1len 14514 |
. . . . . . . . . . . 12
β’ ((π prefix πΈ) β Word π· β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
65 | 51, 64 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
66 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π β π€ = π) |
67 | | dmeq 5860 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π β dom π€ = dom π) |
68 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ = π β π· = π·) |
69 | 66, 67, 68 | f1eq123d 6777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
70 | 69 | elrab3 3647 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word π· β (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β π:dom πβ1-1βπ·)) |
71 | 70 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Word π· β§ π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) β π:dom πβ1-1βπ·) |
72 | 17, 16, 71 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:dom πβ1-1βπ·) |
73 | | f1cnv 6809 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:dom πβ1-1βπ· β β‘π:ran πβ1-1-ontoβdom
π) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β‘π:ran πβ1-1-ontoβdom
π) |
75 | | f1of 6785 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β β‘π:ran πβΆdom π) |
77 | 76, 6 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ (π β (β‘πβπ½) β dom π) |
78 | | wrddm 14415 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
79 | 17, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β dom π = (0..^(β―βπ))) |
80 | 77, 79 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (π β (β‘πβπ½) β (0..^(β―βπ))) |
81 | | fzofzp1 13675 |
. . . . . . . . . . . . . . 15
β’ ((β‘πβπ½) β (0..^(β―βπ)) β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
83 | 7, 82 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β πΈ β (0...(β―βπ))) |
84 | | pfxlen 14577 |
. . . . . . . . . . . . 13
β’ ((π β Word π· β§ πΈ β (0...(β―βπ))) β (β―β(π prefix πΈ)) = πΈ) |
85 | 17, 83, 84 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (β―β(π prefix πΈ)) = πΈ) |
86 | 85 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β ((β―β(π prefix πΈ)) + 1) = (πΈ + 1)) |
87 | 65, 86 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = (πΈ + 1)) |
88 | 87 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΈ β (0..^(β―βπ))) β
(β―β((π prefix
πΈ) ++ β¨βπΌββ©)) = (πΈ + 1)) |
89 | 47 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π β (β―βπ) = (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)))) |
90 | | ccatlen 14469 |
. . . . . . . . . . . . . . 15
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π·) β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
91 | 53, 56, 90 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
92 | | swrdlen 14541 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π· β§ πΈ β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β (β―β(π
substr β¨πΈ,
(β―βπ)β©)) =
((β―βπ) β
πΈ)) |
93 | 17, 83, 39, 92 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β(π substr β¨πΈ, (β―βπ)β©)) = ((β―βπ) β πΈ)) |
94 | 87, 93 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π β ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
95 | 89, 91, 94 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β (β―βπ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
96 | | fz0ssnn0 13542 |
. . . . . . . . . . . . . . . . . 18
β’
(0...(β―βπ)) β
β0 |
97 | 96, 83 | sselid 3943 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΈ β
β0) |
98 | 97 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ β β€) |
99 | 98 | peano2zd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β (πΈ + 1) β β€) |
100 | 99 | zcnd 12613 |
. . . . . . . . . . . . . 14
β’ (π β (πΈ + 1) β β) |
101 | 37 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
β’ (π β (β―βπ) β
β) |
102 | 97 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β β) |
103 | 100, 101,
102 | addsubassd 11537 |
. . . . . . . . . . . . 13
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
104 | | 1cnd 11155 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β
β) |
105 | 102, 104,
101 | addassd 11182 |
. . . . . . . . . . . . . 14
β’ (π β ((πΈ + 1) + (β―βπ)) = (πΈ + (1 + (β―βπ)))) |
106 | 105 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
107 | 95, 103, 106 | 3eqtr2d 2779 |
. . . . . . . . . . . 12
β’ (π β (β―βπ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
108 | 104, 101 | addcld 11179 |
. . . . . . . . . . . . 13
β’ (π β (1 + (β―βπ)) β
β) |
109 | 102, 108 | pncan2d 11519 |
. . . . . . . . . . . 12
β’ (π β ((πΈ + (1 + (β―βπ))) β πΈ) = (1 + (β―βπ))) |
110 | 104, 101 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (π β (1 + (β―βπ)) = ((β―βπ) + 1)) |
111 | 107, 109,
110 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (β―βπ) = ((β―βπ) + 1)) |
112 | 89, 111, 91 | 3eqtr3rd 2782 |
. . . . . . . . . 10
β’ (π β ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))) = ((β―βπ) + 1)) |
113 | 112 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΈ β (0..^(β―βπ))) β
((β―β((π prefix
πΈ) ++ β¨βπΌββ©)) +
(β―β(π substr
β¨πΈ,
(β―βπ)β©)))
= ((β―βπ) +
1)) |
114 | 88, 113 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β§ πΈ β (0..^(β―βπ))) β
((β―β((π prefix
πΈ) ++ β¨βπΌββ©))..^((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) = ((πΈ + 1)..^((β―βπ) + 1))) |
115 | 63, 114 | eleqtrrd 2837 |
. . . . . . 7
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πΈ + 1) β ((β―β((π prefix πΈ) ++ β¨βπΌββ©))..^((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))))) |
116 | | ccatval2 14472 |
. . . . . . 7
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π· β§ (πΈ + 1) β ((β―β((π prefix πΈ) ++ β¨βπΌββ©))..^((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))))) β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β(πΈ + 1)) = ((π substr β¨πΈ, (β―βπ)β©)β((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©))))) |
117 | 54, 57, 115, 116 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β(πΈ + 1)) = ((π substr β¨πΈ, (β―βπ)β©)β((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©))))) |
118 | 87 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β ((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©))) = ((πΈ + 1) β (πΈ + 1))) |
119 | 100 | subidd 11505 |
. . . . . . . . 9
β’ (π β ((πΈ + 1) β (πΈ + 1)) = 0) |
120 | 118, 119 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©))) = 0) |
121 | 120 | fveq2d 6847 |
. . . . . . 7
β’ (π β ((π substr β¨πΈ, (β―βπ)β©)β((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©)))) = ((π substr β¨πΈ, (β―βπ)β©)β0)) |
122 | 121 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((π substr β¨πΈ, (β―βπ)β©)β((πΈ + 1) β (β―β((π prefix πΈ) ++ β¨βπΌββ©)))) = ((π substr β¨πΈ, (β―βπ)β©)β0)) |
123 | 49, 117, 122 | 3eqtrd 2777 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πβ(πΈ + 1)) = ((π substr β¨πΈ, (β―βπ)β©)β0)) |
124 | 7 | fveq2i 6846 |
. . . . . . 7
β’ (πβπΈ) = (πβ((β‘πβπ½) + 1)) |
125 | 124 | a1i 11 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πβπΈ) = (πβ((β‘πβπ½) + 1))) |
126 | 72 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ β (0..^(β―βπ))) β π:dom πβ1-1βπ·) |
127 | 7 | oveq1i 7368 |
. . . . . . . . . 10
β’ (πΈ β 1) = (((β‘πβπ½) + 1) β 1) |
128 | | elfzonn0 13623 |
. . . . . . . . . . . . 13
β’ ((β‘πβπ½) β (0..^(β―βπ)) β (β‘πβπ½) β
β0) |
129 | 80, 128 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β‘πβπ½) β
β0) |
130 | 129 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ (π β (β‘πβπ½) β β) |
131 | 130, 104 | pncand 11518 |
. . . . . . . . . 10
β’ (π β (((β‘πβπ½) + 1) β 1) = (β‘πβπ½)) |
132 | 127, 131 | eqtr2id 2786 |
. . . . . . . . 9
β’ (π β (β‘πβπ½) = (πΈ β 1)) |
133 | 132 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΈ β (0..^(β―βπ))) β (β‘πβπ½) = (πΈ β 1)) |
134 | | nn0p1gt0 12447 |
. . . . . . . . . . . . . 14
β’ ((β‘πβπ½) β β0 β 0 <
((β‘πβπ½) + 1)) |
135 | 129, 134 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((β‘πβπ½) + 1)) |
136 | 135, 7 | breqtrrdi 5148 |
. . . . . . . . . . . 12
β’ (π β 0 < πΈ) |
137 | 136 | gt0ne0d 11724 |
. . . . . . . . . . 11
β’ (π β πΈ β 0) |
138 | 137 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΈ β (0..^(β―βπ))) β πΈ β 0) |
139 | | fzo1fzo0n0 13629 |
. . . . . . . . . 10
β’ (πΈ β
(1..^(β―βπ))
β (πΈ β
(0..^(β―βπ))
β§ πΈ β
0)) |
140 | 26, 138, 139 | sylanbrc 584 |
. . . . . . . . 9
β’ ((π β§ πΈ β (0..^(β―βπ))) β πΈ β (1..^(β―βπ))) |
141 | | elfzo1elm1fzo0 13679 |
. . . . . . . . 9
β’ (πΈ β
(1..^(β―βπ))
β (πΈ β 1) β
(0..^((β―βπ)
β 1))) |
142 | 140, 141 | syl 17 |
. . . . . . . 8
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πΈ β 1) β
(0..^((β―βπ)
β 1))) |
143 | 133, 142 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ πΈ β (0..^(β―βπ))) β (β‘πβπ½) β (0..^((β―βπ) β 1))) |
144 | 1, 10, 35, 126, 143 | cycpmfv1 32011 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)β(πβ(β‘πβπ½))) = (πβ((β‘πβπ½) + 1))) |
145 | | f1f1orn 6796 |
. . . . . . . . . 10
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
146 | 72, 145 | syl 17 |
. . . . . . . . 9
β’ (π β π:dom πβ1-1-ontoβran
π) |
147 | | f1ocnvfv2 7224 |
. . . . . . . . 9
β’ ((π:dom πβ1-1-ontoβran
π β§ π½ β ran π) β (πβ(β‘πβπ½)) = π½) |
148 | 146, 6, 147 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πβ(β‘πβπ½)) = π½) |
149 | 148 | fveq2d 6847 |
. . . . . . 7
β’ (π β ((πβπ)β(πβ(β‘πβπ½))) = ((πβπ)βπ½)) |
150 | 149 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)β(πβ(β‘πβπ½))) = ((πβπ)βπ½)) |
151 | 125, 144,
150 | 3eqtr2rd 2780 |
. . . . 5
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)βπ½) = (πβπΈ)) |
152 | 42, 123, 151 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ πΈ β (0..^(β―βπ))) β (πβ(πΈ + 1)) = ((πβπ)βπ½)) |
153 | 31, 34, 152 | 3eqtr3rd 2782 |
. . 3
β’ ((π β§ πΈ β (0..^(β―βπ))) β ((πβπ)βπ½) = ((πβπ)βπΌ)) |
154 | 149 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)β(πβ(β‘πβπ½))) = ((πβπ)βπ½)) |
155 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β π· β π) |
156 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β π β Word π·) |
157 | 72 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β π:dom πβ1-1βπ·) |
158 | 136 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = (β―βπ)) β 0 < πΈ) |
159 | | simpr 486 |
. . . . . . 7
β’ ((π β§ πΈ = (β―βπ)) β πΈ = (β―βπ)) |
160 | 158, 159 | breqtrd 5132 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β 0 < (β―βπ)) |
161 | | oveq1 7365 |
. . . . . . 7
β’ (πΈ = (β―βπ) β (πΈ β 1) = ((β―βπ) β 1)) |
162 | 132, 161 | sylan9eq 2793 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β (β‘πβπ½) = ((β―βπ) β 1)) |
163 | 1, 155, 156, 157, 160, 162 | cycpmfv2 32012 |
. . . . 5
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)β(πβ(β‘πβπ½))) = (πβ0)) |
164 | 154, 163 | eqtr3d 2775 |
. . . 4
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)βπ½) = (πβ0)) |
165 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β π β Word π·) |
166 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β π:dom πβ1-1βπ·) |
167 | | nn0p1gt0 12447 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β 0 < ((β―βπ) + 1)) |
168 | 37, 167 | syl 17 |
. . . . . . . 8
β’ (π β 0 <
((β―βπ) +
1)) |
169 | 168, 111 | breqtrrd 5134 |
. . . . . . 7
β’ (π β 0 <
(β―βπ)) |
170 | 169 | adantr 482 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β 0 < (β―βπ)) |
171 | 27 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΈ = (β―βπ)) β ((β―βπ) β 1) = (β―βπ)) |
172 | 159, 171 | eqtr4d 2776 |
. . . . . 6
β’ ((π β§ πΈ = (β―βπ)) β πΈ = ((β―βπ) β 1)) |
173 | 1, 155, 165, 166, 170, 172 | cycpmfv2 32012 |
. . . . 5
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)β(πβπΈ)) = (πβ0)) |
174 | 47 | fveq1d 6845 |
. . . . . 6
β’ (π β (πβ0) = ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0)) |
175 | 174 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ = (β―βπ)) β (πβ0) = ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0)) |
176 | | nn0p1nn 12457 |
. . . . . . . . . . 11
β’ (πΈ β β0
β (πΈ + 1) β
β) |
177 | 97, 176 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΈ + 1) β β) |
178 | | lbfzo0 13618 |
. . . . . . . . . 10
β’ (0 β
(0..^(πΈ + 1)) β (πΈ + 1) β
β) |
179 | 177, 178 | sylibr 233 |
. . . . . . . . 9
β’ (π β 0 β (0..^(πΈ + 1))) |
180 | 87 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β
(0..^(β―β((π
prefix πΈ) ++
β¨βπΌββ©))) = (0..^(πΈ + 1))) |
181 | 179, 180 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β 0 β
(0..^(β―β((π
prefix πΈ) ++
β¨βπΌββ©)))) |
182 | | ccatval1 14471 |
. . . . . . . 8
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π· β§ 0 β (0..^(β―β((π prefix πΈ) ++ β¨βπΌββ©)))) β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (((π prefix πΈ) ++ β¨βπΌββ©)β0)) |
183 | 53, 56, 181, 182 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (((π prefix πΈ) ++ β¨βπΌββ©)β0)) |
184 | | nn0p1nn 12457 |
. . . . . . . . . . . 12
β’ ((β‘πβπ½) β β0 β ((β‘πβπ½) + 1) β β) |
185 | 129, 184 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((β‘πβπ½) + 1) β β) |
186 | 7, 185 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π β πΈ β β) |
187 | | lbfzo0 13618 |
. . . . . . . . . 10
β’ (0 β
(0..^πΈ) β πΈ β
β) |
188 | 186, 187 | sylibr 233 |
. . . . . . . . 9
β’ (π β 0 β (0..^πΈ)) |
189 | 85 | oveq2d 7374 |
. . . . . . . . 9
β’ (π β (0..^(β―β(π prefix πΈ))) = (0..^πΈ)) |
190 | 188, 189 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β 0 β
(0..^(β―β(π
prefix πΈ)))) |
191 | | ccatval1 14471 |
. . . . . . . 8
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π· β§ 0 β (0..^(β―β(π prefix πΈ)))) β (((π prefix πΈ) ++ β¨βπΌββ©)β0) = ((π prefix πΈ)β0)) |
192 | 51, 19, 190, 191 | syl3anc 1372 |
. . . . . . 7
β’ (π β (((π prefix πΈ) ++ β¨βπΌββ©)β0) = ((π prefix πΈ)β0)) |
193 | | fzne1 31738 |
. . . . . . . . . 10
β’ ((πΈ β
(0...(β―βπ))
β§ πΈ β 0) β
πΈ β ((0 +
1)...(β―βπ))) |
194 | 83, 137, 193 | syl2anc 585 |
. . . . . . . . 9
β’ (π β πΈ β ((0 + 1)...(β―βπ))) |
195 | | 0p1e1 12280 |
. . . . . . . . . 10
β’ (0 + 1) =
1 |
196 | 195 | oveq1i 7368 |
. . . . . . . . 9
β’ ((0 +
1)...(β―βπ)) =
(1...(β―βπ)) |
197 | 194, 196 | eleqtrdi 2844 |
. . . . . . . 8
β’ (π β πΈ β (1...(β―βπ))) |
198 | | pfxfv0 14586 |
. . . . . . . 8
β’ ((π β Word π· β§ πΈ β (1...(β―βπ))) β ((π prefix πΈ)β0) = (πβ0)) |
199 | 17, 197, 198 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π prefix πΈ)β0) = (πβ0)) |
200 | 183, 192,
199 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (πβ0)) |
201 | 200 | adantr 482 |
. . . . 5
β’ ((π β§ πΈ = (β―βπ)) β ((((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))β0) = (πβ0)) |
202 | 173, 175,
201 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)β(πβπΈ)) = (πβ0)) |
203 | 33 | adantr 482 |
. . . 4
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)β(πβπΈ)) = ((πβπ)βπΌ)) |
204 | 164, 202,
203 | 3eqtr2d 2779 |
. . 3
β’ ((π β§ πΈ = (β―βπ)) β ((πβπ)βπ½) = ((πβπ)βπΌ)) |
205 | | elfzr 13691 |
. . . 4
β’ (πΈ β
(0...(β―βπ))
β (πΈ β
(0..^(β―βπ))
β¨ πΈ =
(β―βπ))) |
206 | 83, 205 | syl 17 |
. . 3
β’ (π β (πΈ β (0..^(β―βπ)) β¨ πΈ = (β―βπ))) |
207 | 153, 204,
206 | mpjaodan 958 |
. 2
β’ (π β ((πβπ)βπ½) = ((πβπ)βπΌ)) |
208 | 9, 207 | eqtrd 2773 |
1
β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπΌ)) |