Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . 3
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . 3
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . 3
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | 1, 2, 3, 4 | efgval2 19513 |
. 2
β’ βΌ =
β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} |
6 | | efgcpbllem.1 |
. . . . . . 7
β’ πΏ = {β¨π, πβ© β£ ({π, π} β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))} |
7 | 6 | relopabiv 5781 |
. . . . . 6
β’ Rel πΏ |
8 | 7 | a1i 11 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β Rel πΏ) |
9 | | efgred.d |
. . . . . . . . 9
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
10 | | efgred.s |
. . . . . . . . 9
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
11 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . . . 8
β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
12 | 11 | simp2bi 1147 |
. . . . . . 7
β’ (ππΏπ β π β π) |
13 | 12 | adantl 483 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β π β π) |
14 | 11 | simp1bi 1146 |
. . . . . . 7
β’ (ππΏπ β π β π) |
15 | 14 | adantl 483 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β π β π) |
16 | 1, 2 | efger 19507 |
. . . . . . . 8
β’ βΌ Er
π |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β βΌ Er π) |
18 | 11 | simp3bi 1148 |
. . . . . . . 8
β’ (ππΏπ β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) |
19 | 18 | adantl 483 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) |
20 | 17, 19 | ersym 8667 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . 6
β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
22 | 13, 15, 20, 21 | syl3anbrc 1344 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ ππΏπ) β ππΏπ) |
23 | 14 | ad2antrl 727 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β π β π) |
24 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . . . 8
β’ (ππΏβ β (π β π β§ β β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ β) ++ π΅))) |
25 | 24 | simp2bi 1147 |
. . . . . . 7
β’ (ππΏβ β β β π) |
26 | 25 | ad2antll 728 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β β β π) |
27 | 16 | a1i 11 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β βΌ Er π) |
28 | 18 | ad2antrl 727 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) |
29 | 24 | simp3bi 1148 |
. . . . . . . 8
β’ (ππΏβ β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ β) ++ π΅)) |
30 | 29 | ad2antll 728 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ β) ++ π΅)) |
31 | 27, 28, 30 | ertrd 8671 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ β) ++ π΅)) |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . 6
β’ (ππΏβ β (π β π β§ β β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ β) ++ π΅))) |
33 | 23, 26, 31, 32 | syl3anbrc 1344 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ (ππΏπ β§ ππΏβ)) β ππΏβ) |
34 | 16 | a1i 11 |
. . . . . . . . 9
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β βΌ Er π) |
35 | | fviss 6923 |
. . . . . . . . . . . . . 14
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
36 | 1, 35 | eqsstri 3983 |
. . . . . . . . . . . . 13
β’ π β Word (πΌ Γ 2o) |
37 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π΄ β π) |
38 | 36, 37 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π΄ β Word (πΌ Γ 2o)) |
39 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π β π) |
40 | 36, 39 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π β Word (πΌ Γ 2o)) |
41 | | ccatcl 14469 |
. . . . . . . . . . . 12
β’ ((π΄ β Word (πΌ Γ 2o) β§ π β Word (πΌ Γ 2o)) β (π΄ ++ π) β Word (πΌ Γ 2o)) |
42 | 38, 40, 41 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β (π΄ ++ π) β Word (πΌ Γ 2o)) |
43 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π΅ β π) |
44 | 36, 43 | sselid 3947 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π΅ β Word (πΌ Γ 2o)) |
45 | | ccatcl 14469 |
. . . . . . . . . . 11
β’ (((π΄ ++ π) β Word (πΌ Γ 2o) β§ π΅ β Word (πΌ Γ 2o)) β ((π΄ ++ π) ++ π΅) β Word (πΌ Γ 2o)) |
46 | 42, 44, 45 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β ((π΄ ++ π) ++ π΅) β Word (πΌ Γ 2o)) |
47 | 1 | efgrcl 19504 |
. . . . . . . . . . . 12
β’ (π΄ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
48 | 47 | simprd 497 |
. . . . . . . . . . 11
β’ (π΄ β π β π = Word (πΌ Γ 2o)) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β π = Word (πΌ Γ 2o)) |
50 | 46, 49 | eleqtrrd 2841 |
. . . . . . . . 9
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β ((π΄ ++ π) ++ π΅) β π) |
51 | 34, 50 | erref 8675 |
. . . . . . . 8
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) |
52 | 51 | ex 414 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β (π β π β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
53 | 52 | pm4.71d 563 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π β π β (π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)))) |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . . 7
β’ (ππΏπ β (π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
55 | | df-3an 1090 |
. . . . . . 7
β’ ((π β π β§ π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β ((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
56 | | anidm 566 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π β π) |
57 | 56 | anbi1i 625 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅)) β (π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
58 | 54, 55, 57 | 3bitri 297 |
. . . . . 6
β’ (ππΏπ β (π β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ π) ++ π΅))) |
59 | 53, 58 | bitr4di 289 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β (π β π β ππΏπ)) |
60 | 8, 22, 33, 59 | iserd 8681 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β πΏ Er π) |
61 | 1, 2, 3, 4 | efgtf 19511 |
. . . . . . . . . 10
β’ (π β π β ((πβπ) = (π β (0...(β―βπ)), π β (πΌ Γ 2o) β¦ (π splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ)) |
62 | 61 | simprd 497 |
. . . . . . . . 9
β’ (π β π β (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
63 | 62 | adantl 483 |
. . . . . . . 8
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
64 | | ffn 6673 |
. . . . . . . 8
β’ ((πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ β (πβπ) Fn ((0...(β―βπ)) Γ (πΌ Γ 2o))) |
65 | | ovelrn 7535 |
. . . . . . . 8
β’ ((πβπ) Fn ((0...(β―βπ)) Γ (πΌ Γ 2o)) β (π β ran (πβπ) β βπ β (0...(β―βπ))βπ’ β (πΌ Γ 2o)π = (π(πβπ)π’))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β (π β ran (πβπ) β βπ β (0...(β―βπ))βπ’ β (πΌ Γ 2o)π = (π(πβπ)π’))) |
67 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π β π) |
68 | 62 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (πβπ):((0...(β―βπ)) Γ (πΌ Γ 2o))βΆπ) |
69 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π β
(0...(β―βπ))) |
70 | | simprr 772 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π’ β (πΌ Γ 2o)) |
71 | 68, 69, 70 | fovcdmd 7531 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π(πβπ)π’) β π) |
72 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ π) ++ π΅) β π) |
73 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π΄ β π) |
74 | 36, 73 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π΄ β Word (πΌ Γ 2o)) |
75 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π β Word (πΌ Γ 2o)) |
76 | | pfxcl 14572 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word (πΌ Γ 2o) β (π prefix π) β Word (πΌ Γ 2o)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π prefix π) β Word (πΌ Γ 2o)) |
78 | | ccatcl 14469 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β Word (πΌ Γ 2o) β§ (π prefix π) β Word (πΌ Γ 2o)) β (π΄ ++ (π prefix π)) β Word (πΌ Γ 2o)) |
79 | 74, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π΄ ++ (π prefix π)) β Word (πΌ Γ 2o)) |
80 | 3 | efgmf 19502 |
. . . . . . . . . . . . . . . . . 18
β’ π:(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
81 | 80 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β (πΌ Γ 2o) β (πβπ’) β (πΌ Γ 2o)) |
82 | 81 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (πβπ’) β (πΌ Γ 2o)) |
83 | 70, 82 | s2cld 14767 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
β¨βπ’(πβπ’)ββ© β Word (πΌ Γ 2o)) |
84 | | ccatcl 14469 |
. . . . . . . . . . . . . . 15
β’ (((π΄ ++ (π prefix π)) β Word (πΌ Γ 2o) β§
β¨βπ’(πβπ’)ββ© β Word (πΌ Γ 2o)) β ((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ
2o)) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ
2o)) |
86 | | swrdcl 14540 |
. . . . . . . . . . . . . . 15
β’ (π β Word (πΌ Γ 2o) β (π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o)) |
87 | 75, 86 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o)) |
88 | 44 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π΅ β Word (πΌ Γ 2o)) |
89 | | ccatass 14483 |
. . . . . . . . . . . . . 14
β’ ((((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ 2o) β§
(π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o) β§
π΅ β Word (πΌ Γ 2o)) β
((((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅) = (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
90 | 85, 87, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅) = (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
91 | | ccatcl 14469 |
. . . . . . . . . . . . . . . . 17
β’ (((π prefix π) β Word (πΌ Γ 2o) β§
β¨βπ’(πβπ’)ββ© β Word (πΌ Γ 2o)) β ((π prefix π) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ
2o)) |
92 | 77, 83, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π prefix π) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ
2o)) |
93 | | ccatass 14483 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β Word (πΌ Γ 2o) β§ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©) β Word (πΌ Γ 2o) β§
(π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o)) β
((π΄ ++ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©)) ++ (π substr β¨π, (β―βπ)β©)) = (π΄ ++ (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)))) |
94 | 74, 92, 87, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©)) ++ (π substr β¨π, (β―βπ)β©)) = (π΄ ++ (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)))) |
95 | | ccatass 14483 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β Word (πΌ Γ 2o) β§ (π prefix π) β Word (πΌ Γ 2o) β§
β¨βπ’(πβπ’)ββ© β Word (πΌ Γ 2o)) β ((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) = (π΄ ++ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©))) |
96 | 74, 77, 83, 95 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) = (π΄ ++ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©))) |
97 | 96 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)) = ((π΄ ++ ((π prefix π) ++ β¨βπ’(πβπ’)ββ©)) ++ (π substr β¨π, (β―βπ)β©))) |
98 | 1, 2, 3, 4 | efgtval 19512 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o)) β (π(πβπ)π’) = (π splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) |
99 | 67, 69, 70, 98 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π(πβπ)π’) = (π splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) |
100 | | splval 14646 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β§ (π β (0...(β―βπ)) β§ π β (0...(β―βπ)) β§ β¨βπ’(πβπ’)ββ© β Word (πΌ Γ 2o))) β (π splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) = (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©))) |
101 | 67, 69, 69, 83, 100 | syl13anc 1373 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π splice β¨π, π, β¨βπ’(πβπ’)ββ©β©) = (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©))) |
102 | 99, 101 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π(πβπ)π’) = (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©))) |
103 | 102 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π΄ ++ (π(πβπ)π’)) = (π΄ ++ (((π prefix π) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)))) |
104 | 94, 97, 103 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π΄ ++ (π(πβπ)π’)) = (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©))) |
105 | 104 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π(πβπ)π’)) ++ π΅) = ((((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅)) |
106 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β Word (πΌ Γ 2o) β
(β―βπ΄) β
β0) |
107 | 74, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ΄) β
β0) |
108 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . . 18
β’
β0 = (β€β₯β0) |
109 | 107, 108 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ΄) β
(β€β₯β0)) |
110 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(0...(β―βπ))
β π β
β0) |
111 | 110 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π β
β0) |
112 | | uzaddcl 12836 |
. . . . . . . . . . . . . . . . 17
β’
(((β―βπ΄)
β (β€β₯β0) β§ π β β0) β
((β―βπ΄) + π) β
(β€β₯β0)) |
113 | 109, 111,
112 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) β
(β€β₯β0)) |
114 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π΄ ++ π) β Word (πΌ Γ 2o)) |
115 | | ccatlen 14470 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ ++ π) β Word (πΌ Γ 2o) β§ π΅ β Word (πΌ Γ 2o)) β
(β―β((π΄ ++ π) ++ π΅)) = ((β―β(π΄ ++ π)) + (β―βπ΅))) |
116 | 114, 88, 115 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β((π΄ ++ π) ++ π΅)) = ((β―β(π΄ ++ π)) + (β―βπ΅))) |
117 | | ccatlen 14470 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β Word (πΌ Γ 2o) β§ π β Word (πΌ Γ 2o)) β
(β―β(π΄ ++ π)) = ((β―βπ΄) + (β―βπ))) |
118 | 74, 75, 117 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β(π΄ ++ π)) = ((β―βπ΄) + (β―βπ))) |
119 | | elfzuz3 13445 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(0...(β―βπ))
β (β―βπ)
β (β€β₯βπ)) |
120 | 119 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ) β
(β€β₯βπ)) |
121 | 107 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ΄) β
β€) |
122 | | eluzadd 12799 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ)
β (β€β₯βπ) β§ (β―βπ΄) β β€) β
((β―βπ) +
(β―βπ΄)) β
(β€β₯β(π + (β―βπ΄)))) |
123 | 120, 121,
122 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ) +
(β―βπ΄)) β
(β€β₯β(π + (β―βπ΄)))) |
124 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Word (πΌ Γ 2o) β
(β―βπ) β
β0) |
125 | 75, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ) β
β0) |
126 | 125 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ) β
β) |
127 | 107 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ΄) β
β) |
128 | 126, 127 | addcomd 11364 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ) +
(β―βπ΄)) =
((β―βπ΄) +
(β―βπ))) |
129 | 111 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β π β
β) |
130 | 129, 127 | addcomd 11364 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π + (β―βπ΄)) = ((β―βπ΄) + π)) |
131 | 130 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β€β₯β(π + (β―βπ΄))) =
(β€β₯β((β―βπ΄) + π))) |
132 | 123, 128,
131 | 3eltr3d 2852 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) +
(β―βπ)) β
(β€β₯β((β―βπ΄) + π))) |
133 | 118, 132 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β(π΄ ++ π)) β
(β€β₯β((β―βπ΄) + π))) |
134 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β Word (πΌ Γ 2o) β
(β―βπ΅) β
β0) |
135 | 88, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ΅) β
β0) |
136 | | uzaddcl 12836 |
. . . . . . . . . . . . . . . . . 18
β’
(((β―β(π΄
++ π)) β
(β€β₯β((β―βπ΄) + π)) β§ (β―βπ΅) β β0) β
((β―β(π΄ ++ π)) + (β―βπ΅)) β
(β€β₯β((β―βπ΄) + π))) |
137 | 133, 135,
136 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―β(π΄ ++ π)) + (β―βπ΅)) β
(β€β₯β((β―βπ΄) + π))) |
138 | 116, 137 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β((π΄ ++ π) ++ π΅)) β
(β€β₯β((β―βπ΄) + π))) |
139 | | elfzuzb 13442 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ΄)
+ π) β
(0...(β―β((π΄ ++
π) ++ π΅))) β (((β―βπ΄) + π) β (β€β₯β0)
β§ (β―β((π΄ ++
π) ++ π΅)) β
(β€β₯β((β―βπ΄) + π)))) |
140 | 113, 138,
139 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) β
(0...(β―β((π΄ ++
π) ++ π΅)))) |
141 | 1, 2, 3, 4 | efgtval 19512 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ ++ π) ++ π΅) β π β§ ((β―βπ΄) + π) β (0...(β―β((π΄ ++ π) ++ π΅))) β§ π’ β (πΌ Γ 2o)) β
(((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’) = (((π΄ ++ π) ++ π΅) splice β¨((β―βπ΄) + π), ((β―βπ΄) + π), β¨βπ’(πβπ’)ββ©β©)) |
142 | 72, 140, 70, 141 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’) = (((π΄ ++ π) ++ π΅) splice β¨((β―βπ΄) + π), ((β―βπ΄) + π), β¨βπ’(πβπ’)ββ©β©)) |
143 | | wrd0 14434 |
. . . . . . . . . . . . . . . 16
β’ β
β Word (πΌ Γ
2o) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β β
β Word (πΌ Γ
2o)) |
145 | | ccatcl 14469 |
. . . . . . . . . . . . . . . 16
β’ (((π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o) β§ π΅ β Word (πΌ Γ 2o)) β ((π substr β¨π, (β―βπ)β©) ++ π΅) β Word (πΌ Γ 2o)) |
146 | 87, 88, 145 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π substr β¨π, (β―βπ)β©) ++ π΅) β Word (πΌ Γ 2o)) |
147 | | ccatrid 14482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ ++ (π prefix π)) β Word (πΌ Γ 2o) β ((π΄ ++ (π prefix π)) ++ β
) = (π΄ ++ (π prefix π))) |
148 | 79, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π prefix π)) ++ β
) = (π΄ ++ (π prefix π))) |
149 | 148 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (((π΄ ++ (π prefix π)) ++ β
) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅)) = ((π΄ ++ (π prefix π)) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
150 | | ccatass 14483 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ ++ (π prefix π)) β Word (πΌ Γ 2o) β§ (π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o) β§ π΅ β Word (πΌ Γ 2o)) β (((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅) = ((π΄ ++ (π prefix π)) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
151 | 79, 87, 88, 150 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅) = ((π΄ ++ (π prefix π)) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
152 | | ccatass 14483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β Word (πΌ Γ 2o) β§ (π prefix π) β Word (πΌ Γ 2o) β§ (π substr β¨π, (β―βπ)β©) β Word (πΌ Γ 2o)) β ((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) = (π΄ ++ ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)))) |
153 | 74, 77, 87, 152 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) = (π΄ ++ ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)))) |
154 | 125, 108 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ) β
(β€β₯β0)) |
155 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ)
β (β€β₯β0) β (β―βπ) β
(0...(β―βπ))) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―βπ) β
(0...(β―βπ))) |
157 | | ccatpfx 14596 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Word (πΌ Γ 2o) β§ π β
(0...(β―βπ))
β§ (β―βπ)
β (0...(β―βπ))) β ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)) = (π prefix (β―βπ))) |
158 | 75, 69, 156, 157 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)) = (π prefix (β―βπ))) |
159 | | pfxid 14579 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Word (πΌ Γ 2o) β (π prefix (β―βπ)) = π) |
160 | 75, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π prefix (β―βπ)) = π) |
161 | 158, 160 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π prefix π) ++ (π substr β¨π, (β―βπ)β©)) = π) |
162 | 161 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π΄ ++ ((π prefix π) ++ (π substr β¨π, (β―βπ)β©))) = (π΄ ++ π)) |
163 | 153, 162 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) = (π΄ ++ π)) |
164 | 163 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (((π΄ ++ (π prefix π)) ++ (π substr β¨π, (β―βπ)β©)) ++ π΅) = ((π΄ ++ π) ++ π΅)) |
165 | 149, 151,
164 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ π) ++ π΅) = (((π΄ ++ (π prefix π)) ++ β
) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
166 | | ccatlen 14470 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β Word (πΌ Γ 2o) β§ (π prefix π) β Word (πΌ Γ 2o)) β
(β―β(π΄ ++ (π prefix π))) = ((β―βπ΄) + (β―β(π prefix π)))) |
167 | 74, 77, 166 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β(π΄ ++ (π prefix π))) = ((β―βπ΄) + (β―β(π prefix π)))) |
168 | | pfxlen 14578 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Word (πΌ Γ 2o) β§ π β
(0...(β―βπ)))
β (β―β(π
prefix π)) = π) |
169 | 75, 69, 168 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(β―β(π prefix
π)) = π) |
170 | 169 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) +
(β―β(π prefix
π))) =
((β―βπ΄) + π)) |
171 | 167, 170 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) = (β―β(π΄ ++ (π prefix π)))) |
172 | | hash0 14274 |
. . . . . . . . . . . . . . . . 17
β’
(β―ββ
) = 0 |
173 | 172 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ΄)
+ π) +
(β―ββ
)) = (((β―βπ΄) + π) + 0) |
174 | 107, 111 | nn0addcld 12484 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) β
β0) |
175 | 174 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) β
β) |
176 | 175 | addid1d 11362 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(((β―βπ΄) + π) + 0) = ((β―βπ΄) + π)) |
177 | 173, 176 | eqtr2id 2790 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
((β―βπ΄) + π) = (((β―βπ΄) + π) +
(β―ββ
))) |
178 | 79, 144, 146, 83, 165, 171, 177 | splval2 14652 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (((π΄ ++ π) ++ π΅) splice β¨((β―βπ΄) + π), ((β―βπ΄) + π), β¨βπ’(πβπ’)ββ©β©) = (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
179 | 142, 178 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’) = (((π΄ ++ (π prefix π)) ++ β¨βπ’(πβπ’)ββ©) ++ ((π substr β¨π, (β―βπ)β©) ++ π΅))) |
180 | 90, 105, 179 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π(πβπ)π’)) ++ π΅) = (((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’)) |
181 | 1, 2, 3, 4 | efgtf 19511 |
. . . . . . . . . . . . . . 15
β’ (((π΄ ++ π) ++ π΅) β π β ((πβ((π΄ ++ π) ++ π΅)) = (π β (0...(β―β((π΄ ++ π) ++ π΅))), π β (πΌ Γ 2o) β¦ (((π΄ ++ π) ++ π΅) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ((π΄ ++ π) ++ π΅)):((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o))βΆπ)) |
182 | 181 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π΄ ++ π) ++ π΅) β π β (πβ((π΄ ++ π) ++ π΅)):((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o))βΆπ) |
183 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’ ((πβ((π΄ ++ π) ++ π΅)):((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o))βΆπ β (πβ((π΄ ++ π) ++ π΅)) Fn ((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o))) |
184 | 72, 182, 183 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (πβ((π΄ ++ π) ++ π΅)) Fn ((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o))) |
185 | | fnovrn 7534 |
. . . . . . . . . . . . 13
β’ (((πβ((π΄ ++ π) ++ π΅)) Fn ((0...(β―β((π΄ ++ π) ++ π΅))) Γ (πΌ Γ 2o)) β§
((β―βπ΄) + π) β
(0...(β―β((π΄ ++
π) ++ π΅))) β§ π’ β (πΌ Γ 2o)) β
(((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’) β ran (πβ((π΄ ++ π) ++ π΅))) |
186 | 184, 140,
70, 185 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β
(((β―βπ΄) + π)(πβ((π΄ ++ π) ++ π΅))π’) β ran (πβ((π΄ ++ π) ++ π΅))) |
187 | 180, 186 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ (π(πβπ)π’)) ++ π΅) β ran (πβ((π΄ ++ π) ++ π΅))) |
188 | 1, 2, 3, 4 | efgi2 19514 |
. . . . . . . . . . 11
β’ ((((π΄ ++ π) ++ π΅) β π β§ ((π΄ ++ (π(πβπ)π’)) ++ π΅) β ran (πβ((π΄ ++ π) ++ π΅))) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ (π(πβπ)π’)) ++ π΅)) |
189 | 72, 187, 188 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ (π(πβπ)π’)) ++ π΅)) |
190 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19543 |
. . . . . . . . . 10
β’ (ππΏ(π(πβπ)π’) β (π β π β§ (π(πβπ)π’) β π β§ ((π΄ ++ π) ++ π΅) βΌ ((π΄ ++ (π(πβπ)π’)) ++ π΅))) |
191 | 67, 71, 189, 190 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β ππΏ(π(πβπ)π’)) |
192 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
193 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
194 | 192, 193 | elec 8699 |
. . . . . . . . . 10
β’ (π β [π]πΏ β ππΏπ) |
195 | | breq2 5114 |
. . . . . . . . . 10
β’ (π = (π(πβπ)π’) β (ππΏπ β ππΏ(π(πβπ)π’))) |
196 | 194, 195 | bitrid 283 |
. . . . . . . . 9
β’ (π = (π(πβπ)π’) β (π β [π]πΏ β ππΏ(π(πβπ)π’))) |
197 | 191, 196 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((((π΄ β π β§ π΅ β π) β§ π β π) β§ (π β (0...(β―βπ)) β§ π’ β (πΌ Γ 2o))) β (π = (π(πβπ)π’) β π β [π]πΏ)) |
198 | 197 | rexlimdvva 3206 |
. . . . . . 7
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β (βπ β (0...(β―βπ))βπ’ β (πΌ Γ 2o)π = (π(πβπ)π’) β π β [π]πΏ)) |
199 | 66, 198 | sylbid 239 |
. . . . . 6
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β (π β ran (πβπ) β π β [π]πΏ)) |
200 | 199 | ssrdv 3955 |
. . . . 5
β’ (((π΄ β π β§ π΅ β π) β§ π β π) β ran (πβπ) β [π]πΏ) |
201 | 200 | ralrimiva 3144 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β βπ β π ran (πβπ) β [π]πΏ) |
202 | 1 | fvexi 6861 |
. . . . . 6
β’ π β V |
203 | | erex 8679 |
. . . . . 6
β’ (πΏ Er π β (π β V β πΏ β V)) |
204 | 60, 202, 203 | mpisyl 21 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β πΏ β V) |
205 | | ereq1 8662 |
. . . . . . 7
β’ (π = πΏ β (π Er π β πΏ Er π)) |
206 | | eceq2 8695 |
. . . . . . . . 9
β’ (π = πΏ β [π]π = [π]πΏ) |
207 | 206 | sseq2d 3981 |
. . . . . . . 8
β’ (π = πΏ β (ran (πβπ) β [π]π β ran (πβπ) β [π]πΏ)) |
208 | 207 | ralbidv 3175 |
. . . . . . 7
β’ (π = πΏ β (βπ β π ran (πβπ) β [π]π β βπ β π ran (πβπ) β [π]πΏ)) |
209 | 205, 208 | anbi12d 632 |
. . . . . 6
β’ (π = πΏ β ((π Er π β§ βπ β π ran (πβπ) β [π]π) β (πΏ Er π β§ βπ β π ran (πβπ) β [π]πΏ))) |
210 | 209 | elabg 3633 |
. . . . 5
β’ (πΏ β V β (πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β (πΏ Er π β§ βπ β π ran (πβπ) β [π]πΏ))) |
211 | 204, 210 | syl 17 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β (πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β (πΏ Er π β§ βπ β π ran (πβπ) β [π]πΏ))) |
212 | 60, 201, 211 | mpbir2and 712 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)}) |
213 | | intss1 4929 |
. . 3
β’ (πΏ β {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β πΏ) |
214 | 212, 213 | syl 17 |
. 2
β’ ((π΄ β π β§ π΅ β π) β β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β πΏ) |
215 | 5, 214 | eqsstrid 3997 |
1
β’ ((π΄ β π β§ π΅ β π) β βΌ β πΏ) |