Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | fviss 6923 |
. . . 4
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
3 | 1, 2 | eqsstri 3983 |
. . 3
β’ π β Word (πΌ Γ 2o) |
4 | 3 | sseli 3945 |
. 2
β’ (π΄ β π β π΄ β Word (πΌ Γ 2o)) |
5 | | id 22 |
. . . . . 6
β’ (π = β
β π = β
) |
6 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = β
β
(reverseβπ) =
(reverseββ
)) |
7 | | rev0 14659 |
. . . . . . . . 9
β’
(reverseββ
) = β
|
8 | 6, 7 | eqtrdi 2793 |
. . . . . . . 8
β’ (π = β
β
(reverseβπ) =
β
) |
9 | 8 | coeq2d 5823 |
. . . . . . 7
β’ (π = β
β (π β (reverseβπ)) = (π β β
)) |
10 | | co02 6217 |
. . . . . . 7
β’ (π β β
) =
β
|
11 | 9, 10 | eqtrdi 2793 |
. . . . . 6
β’ (π = β
β (π β (reverseβπ)) = β
) |
12 | 5, 11 | oveq12d 7380 |
. . . . 5
β’ (π = β
β (π ++ (π β (reverseβπ))) = (β
++ β
)) |
13 | 12 | breq1d 5120 |
. . . 4
β’ (π = β
β ((π ++ (π β (reverseβπ))) βΌ β
β
(β
++ β
) βΌ
β
)) |
14 | 13 | imbi2d 341 |
. . 3
β’ (π = β
β ((π΄ β π β (π ++ (π β (reverseβπ))) βΌ β
) β
(π΄ β π β (β
++ β
) βΌ
β
))) |
15 | | id 22 |
. . . . . 6
β’ (π = π β π = π) |
16 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (reverseβπ) = (reverseβπ)) |
17 | 16 | coeq2d 5823 |
. . . . . 6
β’ (π = π β (π β (reverseβπ)) = (π β (reverseβπ))) |
18 | 15, 17 | oveq12d 7380 |
. . . . 5
β’ (π = π β (π ++ (π β (reverseβπ))) = (π ++ (π β (reverseβπ)))) |
19 | 18 | breq1d 5120 |
. . . 4
β’ (π = π β ((π ++ (π β (reverseβπ))) βΌ β
β
(π ++ (π β (reverseβπ))) βΌ
β
)) |
20 | 19 | imbi2d 341 |
. . 3
β’ (π = π β ((π΄ β π β (π ++ (π β (reverseβπ))) βΌ β
) β
(π΄ β π β (π ++ (π β (reverseβπ))) βΌ
β
))) |
21 | | id 22 |
. . . . . 6
β’ (π = (π ++ β¨βπββ©) β π = (π ++ β¨βπββ©)) |
22 | | fveq2 6847 |
. . . . . . 7
β’ (π = (π ++ β¨βπββ©) β (reverseβπ) = (reverseβ(π ++ β¨βπββ©))) |
23 | 22 | coeq2d 5823 |
. . . . . 6
β’ (π = (π ++ β¨βπββ©) β (π β (reverseβπ)) = (π β (reverseβ(π ++ β¨βπββ©)))) |
24 | 21, 23 | oveq12d 7380 |
. . . . 5
β’ (π = (π ++ β¨βπββ©) β (π ++ (π β (reverseβπ))) = ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©))))) |
25 | 24 | breq1d 5120 |
. . . 4
β’ (π = (π ++ β¨βπββ©) β ((π ++ (π β (reverseβπ))) βΌ β
β
((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
)) |
26 | 25 | imbi2d 341 |
. . 3
β’ (π = (π ++ β¨βπββ©) β ((π΄ β π β (π ++ (π β (reverseβπ))) βΌ β
) β
(π΄ β π β ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
))) |
27 | | id 22 |
. . . . . 6
β’ (π = π΄ β π = π΄) |
28 | | fveq2 6847 |
. . . . . . 7
β’ (π = π΄ β (reverseβπ) = (reverseβπ΄)) |
29 | 28 | coeq2d 5823 |
. . . . . 6
β’ (π = π΄ β (π β (reverseβπ)) = (π β (reverseβπ΄))) |
30 | 27, 29 | oveq12d 7380 |
. . . . 5
β’ (π = π΄ β (π ++ (π β (reverseβπ))) = (π΄ ++ (π β (reverseβπ΄)))) |
31 | 30 | breq1d 5120 |
. . . 4
β’ (π = π΄ β ((π ++ (π β (reverseβπ))) βΌ β
β
(π΄ ++ (π β (reverseβπ΄))) βΌ
β
)) |
32 | 31 | imbi2d 341 |
. . 3
β’ (π = π΄ β ((π΄ β π β (π ++ (π β (reverseβπ))) βΌ β
) β
(π΄ β π β (π΄ ++ (π β (reverseβπ΄))) βΌ
β
))) |
33 | | ccatidid 14485 |
. . . 4
β’ (β
++ β
) = β
|
34 | | efgval.r |
. . . . . . 7
β’ βΌ = (
~FG βπΌ) |
35 | 1, 34 | efger 19507 |
. . . . . 6
β’ βΌ Er
π |
36 | 35 | a1i 11 |
. . . . 5
β’ (π΄ β π β βΌ Er π) |
37 | | wrd0 14434 |
. . . . . 6
β’ β
β Word (πΌ Γ
2o) |
38 | 1 | efgrcl 19504 |
. . . . . . 7
β’ (π΄ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
39 | 38 | simprd 497 |
. . . . . 6
β’ (π΄ β π β π = Word (πΌ Γ 2o)) |
40 | 37, 39 | eleqtrrid 2845 |
. . . . 5
β’ (π΄ β π β β
β π) |
41 | 36, 40 | erref 8675 |
. . . 4
β’ (π΄ β π β β
βΌ
β
) |
42 | 33, 41 | eqbrtrid 5145 |
. . 3
β’ (π΄ β π β (β
++ β
) βΌ
β
) |
43 | 35 | a1i 11 |
. . . . . . 7
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β βΌ Er
π) |
44 | | simprl 770 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β π β Word (πΌ Γ 2o)) |
45 | | revcl 14656 |
. . . . . . . . . . . 12
β’ (π β Word (πΌ Γ 2o) β
(reverseβπ) β
Word (πΌ Γ
2o)) |
46 | 45 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(reverseβπ) β
Word (πΌ Γ
2o)) |
47 | | efgval2.m |
. . . . . . . . . . . 12
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
48 | 47 | efgmf 19502 |
. . . . . . . . . . 11
β’ π:(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
49 | | wrdco 14727 |
. . . . . . . . . . 11
β’
(((reverseβπ)
β Word (πΌ Γ
2o) β§ π:(πΌ Γ 2o)βΆ(πΌ Γ 2o)) β
(π β
(reverseβπ)) β
Word (πΌ Γ
2o)) |
50 | 46, 48, 49 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π β (reverseβπ)) β Word (πΌ Γ
2o)) |
51 | | ccatcl 14469 |
. . . . . . . . . 10
β’ ((π β Word (πΌ Γ 2o) β§ (π β (reverseβπ)) β Word (πΌ Γ 2o)) β
(π ++ (π β (reverseβπ))) β Word (πΌ Γ 2o)) |
52 | 44, 50, 51 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ (π β (reverseβπ))) β Word (πΌ Γ 2o)) |
53 | 39 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β π = Word (πΌ Γ 2o)) |
54 | 52, 53 | eleqtrrd 2841 |
. . . . . . . 8
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ (π β (reverseβπ))) β π) |
55 | | lencl 14428 |
. . . . . . . . . . . . . 14
β’ (π β Word (πΌ Γ 2o) β
(β―βπ) β
β0) |
56 | 55 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
β0) |
57 | | nn0uz 12812 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
58 | 56, 57 | eleqtrdi 2848 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
(β€β₯β0)) |
59 | | ccatlen 14470 |
. . . . . . . . . . . . . 14
β’ ((π β Word (πΌ Γ 2o) β§ (π β (reverseβπ)) β Word (πΌ Γ 2o)) β
(β―β(π ++ (π β (reverseβπ)))) = ((β―βπ) + (β―β(π β (reverseβπ))))) |
60 | 44, 50, 59 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―β(π ++ (π β (reverseβπ)))) = ((β―βπ) + (β―β(π β (reverseβπ))))) |
61 | 56 | nn0zd 12532 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
β€) |
62 | 61 | uzidd 12786 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
(β€β₯β(β―βπ))) |
63 | | lencl 14428 |
. . . . . . . . . . . . . . 15
β’ ((π β (reverseβπ)) β Word (πΌ Γ 2o) β
(β―β(π β
(reverseβπ))) β
β0) |
64 | 50, 63 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―β(π β
(reverseβπ))) β
β0) |
65 | | uzaddcl 12836 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
β (β€β₯β(β―βπ)) β§ (β―β(π β (reverseβπ))) β β0) β
((β―βπ) +
(β―β(π β
(reverseβπ)))) β
(β€β₯β(β―βπ))) |
66 | 62, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
((β―βπ) +
(β―β(π β
(reverseβπ)))) β
(β€β₯β(β―βπ))) |
67 | 60, 66 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―β(π ++ (π β (reverseβπ)))) β
(β€β₯β(β―βπ))) |
68 | | elfzuzb 13442 |
. . . . . . . . . . . 12
β’
((β―βπ)
β (0...(β―β(π ++ (π β (reverseβπ))))) β ((β―βπ) β
(β€β₯β0) β§ (β―β(π ++ (π β (reverseβπ)))) β
(β€β₯β(β―βπ)))) |
69 | 58, 67, 68 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
(0...(β―β(π ++
(π β
(reverseβπ)))))) |
70 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β π β (πΌ Γ 2o)) |
71 | | efgval2.t |
. . . . . . . . . . . 12
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
72 | 1, 34, 47, 71 | efgtval 19512 |
. . . . . . . . . . 11
β’ (((π ++ (π β (reverseβπ))) β π β§ (β―βπ) β (0...(β―β(π ++ (π β (reverseβπ))))) β§ π β (πΌ Γ 2o)) β
((β―βπ)(πβ(π ++ (π β (reverseβπ))))π) = ((π ++ (π β (reverseβπ))) splice β¨(β―βπ), (β―βπ), β¨βπ(πβπ)ββ©β©)) |
73 | 54, 69, 70, 72 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
((β―βπ)(πβ(π ++ (π β (reverseβπ))))π) = ((π ++ (π β (reverseβπ))) splice β¨(β―βπ), (β―βπ), β¨βπ(πβπ)ββ©β©)) |
74 | 37 | a1i 11 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β β
β Word (πΌ Γ
2o)) |
75 | 48 | ffvelcdmi 7039 |
. . . . . . . . . . . . 13
β’ (π β (πΌ Γ 2o) β (πβπ) β (πΌ Γ 2o)) |
76 | 75 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (πβπ) β (πΌ Γ 2o)) |
77 | 70, 76 | s2cld 14767 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o)) |
78 | | ccatrid 14482 |
. . . . . . . . . . . . . 14
β’ (π β Word (πΌ Γ 2o) β (π ++ β
) = π) |
79 | 78 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ β
) = π) |
80 | 79 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β π = (π ++ β
)) |
81 | 80 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ (π β (reverseβπ))) = ((π ++ β
) ++ (π β (reverseβπ)))) |
82 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) =
(β―βπ)) |
83 | | hash0 14274 |
. . . . . . . . . . . . 13
β’
(β―ββ
) = 0 |
84 | 83 | oveq2i 7373 |
. . . . . . . . . . . 12
β’
((β―βπ) +
(β―ββ
)) = ((β―βπ) + 0) |
85 | 56 | nn0cnd 12482 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) β
β) |
86 | 85 | addid1d 11362 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
((β―βπ) + 0) =
(β―βπ)) |
87 | 84, 86 | eqtr2id 2790 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(β―βπ) =
((β―βπ) +
(β―ββ
))) |
88 | 44, 74, 50, 77, 81, 82, 87 | splval2 14652 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ (π β (reverseβπ))) splice β¨(β―βπ), (β―βπ), β¨βπ(πβπ)ββ©β©) = ((π ++ β¨βπ(πβπ)ββ©) ++ (π β (reverseβπ)))) |
89 | 70 | s1cld 14498 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
β¨βπββ©
β Word (πΌ Γ
2o)) |
90 | | revccat 14661 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word (πΌ Γ 2o) β§
β¨βπββ©
β Word (πΌ Γ
2o)) β (reverseβ(π ++ β¨βπββ©)) =
((reverseββ¨βπββ©) ++ (reverseβπ))) |
91 | 44, 89, 90 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(reverseβ(π ++
β¨βπββ©)) =
((reverseββ¨βπββ©) ++ (reverseβπ))) |
92 | | revs1 14660 |
. . . . . . . . . . . . . . . 16
β’
(reverseββ¨βπββ©) = β¨βπββ© |
93 | 92 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’
((reverseββ¨βπββ©) ++ (reverseβπ)) = (β¨βπββ© ++
(reverseβπ)) |
94 | 91, 93 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
(reverseβ(π ++
β¨βπββ©)) = (β¨βπββ© ++
(reverseβπ))) |
95 | 94 | coeq2d 5823 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π β (reverseβ(π ++ β¨βπββ©))) = (π β (β¨βπββ© ++
(reverseβπ)))) |
96 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β π:(πΌ Γ 2o)βΆ(πΌ Γ
2o)) |
97 | | ccatco 14731 |
. . . . . . . . . . . . . 14
β’
((β¨βπββ© β Word (πΌ Γ 2o) β§
(reverseβπ) β
Word (πΌ Γ
2o) β§ π:(πΌ Γ 2o)βΆ(πΌ Γ 2o)) β
(π β
(β¨βπββ© ++ (reverseβπ))) = ((π β β¨βπββ©) ++ (π β (reverseβπ)))) |
98 | 89, 46, 96, 97 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π β (β¨βπββ© ++
(reverseβπ))) =
((π β
β¨βπββ©) ++ (π β (reverseβπ)))) |
99 | | s1co 14729 |
. . . . . . . . . . . . . . 15
β’ ((π β (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆ(πΌ Γ 2o)) β
(π β
β¨βπββ©) = β¨β(πβπ)ββ©) |
100 | 70, 48, 99 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π β β¨βπββ©) =
β¨β(πβπ)ββ©) |
101 | 100 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π β β¨βπββ©) ++ (π β (reverseβπ))) = (β¨β(πβπ)ββ© ++ (π β (reverseβπ)))) |
102 | 95, 98, 101 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π β (reverseβ(π ++ β¨βπββ©))) =
(β¨β(πβπ)ββ© ++ (π β (reverseβπ)))) |
103 | 102 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) = ((π ++ β¨βπββ©) ++
(β¨β(πβπ)ββ© ++ (π β (reverseβπ))))) |
104 | | ccatcl 14469 |
. . . . . . . . . . . . 13
β’ ((π β Word (πΌ Γ 2o) β§
β¨βπββ©
β Word (πΌ Γ
2o)) β (π
++ β¨βπββ©) β Word (πΌ Γ 2o)) |
105 | 44, 89, 104 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ β¨βπββ©) β Word
(πΌ Γ
2o)) |
106 | 76 | s1cld 14498 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
β¨β(πβπ)ββ© β Word
(πΌ Γ
2o)) |
107 | | ccatass 14483 |
. . . . . . . . . . . 12
β’ (((π ++ β¨βπββ©) β Word
(πΌ Γ 2o)
β§ β¨β(πβπ)ββ© β Word (πΌ Γ 2o) β§ (π β (reverseβπ)) β Word (πΌ Γ 2o)) β
(((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) ++ (π β (reverseβπ))) = ((π ++ β¨βπββ©) ++ (β¨β(πβπ)ββ© ++ (π β (reverseβπ))))) |
108 | 105, 106,
50, 107 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) ++ (π β (reverseβπ))) = ((π ++ β¨βπββ©) ++ (β¨β(πβπ)ββ© ++ (π β (reverseβπ))))) |
109 | | ccatass 14483 |
. . . . . . . . . . . . . 14
β’ ((π β Word (πΌ Γ 2o) β§
β¨βπββ©
β Word (πΌ Γ
2o) β§ β¨β(πβπ)ββ© β Word (πΌ Γ 2o)) β ((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) = (π ++ (β¨βπββ© ++
β¨β(πβπ)ββ©))) |
110 | 44, 89, 106, 109 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) = (π ++ (β¨βπββ© ++
β¨β(πβπ)ββ©))) |
111 | | df-s2 14744 |
. . . . . . . . . . . . . 14
β’
β¨βπ(πβπ)ββ© = (β¨βπββ© ++
β¨β(πβπ)ββ©) |
112 | 111 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’ (π ++ β¨βπ(πβπ)ββ©) = (π ++ (β¨βπββ© ++ β¨β(πβπ)ββ©)) |
113 | 110, 112 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) = (π ++ β¨βπ(πβπ)ββ©)) |
114 | 113 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (((π ++ β¨βπββ©) ++
β¨β(πβπ)ββ©) ++ (π β (reverseβπ))) = ((π ++ β¨βπ(πβπ)ββ©) ++ (π β (reverseβπ)))) |
115 | 103, 108,
114 | 3eqtr2rd 2784 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπ(πβπ)ββ©) ++ (π β (reverseβπ))) = ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©))))) |
116 | 73, 88, 115 | 3eqtrd 2781 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
((β―βπ)(πβ(π ++ (π β (reverseβπ))))π) = ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©))))) |
117 | 1, 34, 47, 71 | efgtf 19511 |
. . . . . . . . . . . . 13
β’ ((π ++ (π β (reverseβπ))) β π β ((πβ(π ++ (π β (reverseβπ)))) = (π β (0...(β―β(π ++ (π β (reverseβπ))))), π’ β (πΌ Γ 2o) β¦ ((π ++ (π β (reverseβπ))) splice β¨π, π, β¨βπ’(πβπ’)ββ©β©)) β§ (πβ(π ++ (π β (reverseβπ)))):((0...(β―β(π ++ (π β (reverseβπ))))) Γ (πΌ Γ 2o))βΆπ)) |
118 | 117 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π ++ (π β (reverseβπ))) β π β (πβ(π ++ (π β (reverseβπ)))):((0...(β―β(π ++ (π β (reverseβπ))))) Γ (πΌ Γ 2o))βΆπ) |
119 | 54, 118 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (πβ(π ++ (π β (reverseβπ)))):((0...(β―β(π ++ (π β (reverseβπ))))) Γ (πΌ Γ 2o))βΆπ) |
120 | 119 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (πβ(π ++ (π β (reverseβπ)))) Fn ((0...(β―β(π ++ (π β (reverseβπ))))) Γ (πΌ Γ 2o))) |
121 | | fnovrn 7534 |
. . . . . . . . . 10
β’ (((πβ(π ++ (π β (reverseβπ)))) Fn ((0...(β―β(π ++ (π β (reverseβπ))))) Γ (πΌ Γ 2o)) β§
(β―βπ) β
(0...(β―β(π ++
(π β
(reverseβπ))))) β§
π β (πΌ Γ 2o)) β
((β―βπ)(πβ(π ++ (π β (reverseβπ))))π) β ran (πβ(π ++ (π β (reverseβπ))))) |
122 | 120, 69, 70, 121 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β
((β―βπ)(πβ(π ++ (π β (reverseβπ))))π) β ran (πβ(π ++ (π β (reverseβπ))))) |
123 | 116, 122 | eqeltrrd 2839 |
. . . . . . . 8
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) β ran
(πβ(π ++ (π β (reverseβπ))))) |
124 | 1, 34, 47, 71 | efgi2 19514 |
. . . . . . . 8
β’ (((π ++ (π β (reverseβπ))) β π β§ ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) β ran (πβ(π ++ (π β (reverseβπ))))) β (π ++ (π β (reverseβπ))) βΌ ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©))))) |
125 | 54, 123, 124 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β (π ++ (π β (reverseβπ))) βΌ ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©))))) |
126 | 43, 125 | ersym 8667 |
. . . . . 6
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ (π ++ (π β (reverseβπ)))) |
127 | 43 | ertr 8670 |
. . . . . 6
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ (π ++ (π β (reverseβπ))) β§ (π ++ (π β (reverseβπ))) βΌ β
) β
((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
)) |
128 | 126, 127 | mpand 694 |
. . . . 5
β’ ((π΄ β π β§ (π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o))) β ((π ++ (π β (reverseβπ))) βΌ β
β
((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
)) |
129 | 128 | expcom 415 |
. . . 4
β’ ((π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β (π΄ β π β ((π ++ (π β (reverseβπ))) βΌ β
β
((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
))) |
130 | 129 | a2d 29 |
. . 3
β’ ((π β Word (πΌ Γ 2o) β§ π β (πΌ Γ 2o)) β ((π΄ β π β (π ++ (π β (reverseβπ))) βΌ β
) β
(π΄ β π β ((π ++ β¨βπββ©) ++ (π β (reverseβ(π ++ β¨βπββ©)))) βΌ
β
))) |
131 | 14, 20, 26, 32, 42, 130 | wrdind 14617 |
. 2
β’ (π΄ β Word (πΌ Γ 2o) β (π΄ β π β (π΄ ++ (π β (reverseβπ΄))) βΌ
β
)) |
132 | 4, 131 | mpcom 38 |
1
β’ (π΄ β π β (π΄ ++ (π β (reverseβπ΄))) βΌ
β
) |