Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
efgval2.m |
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) |
4 |
|
efgval2.t |
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) |
5 |
|
efgred.d |
|- D = ( W \ U_ x e. W ran ( T ` x ) ) |
6 |
|
efgred.s |
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) ) |
7 |
|
efgredlem.1 |
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) |
8 |
|
efgredlem.2 |
|- ( ph -> A e. dom S ) |
9 |
|
efgredlem.3 |
|- ( ph -> B e. dom S ) |
10 |
|
efgredlem.4 |
|- ( ph -> ( S ` A ) = ( S ` B ) ) |
11 |
|
efgredlem.5 |
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) ) |
12 |
|
efgredlemb.k |
|- K = ( ( ( # ` A ) - 1 ) - 1 ) |
13 |
|
efgredlemb.l |
|- L = ( ( ( # ` B ) - 1 ) - 1 ) |
14 |
|
efgredlemb.p |
|- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) ) |
15 |
|
efgredlemb.q |
|- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) ) |
16 |
|
efgredlemb.u |
|- ( ph -> U e. ( I X. 2o ) ) |
17 |
|
efgredlemb.v |
|- ( ph -> V e. ( I X. 2o ) ) |
18 |
|
efgredlemb.6 |
|- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) ) |
19 |
|
efgredlemb.7 |
|- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) ) |
20 |
|
efgredlemb.8 |
|- ( ph -> -. ( A ` K ) = ( B ` L ) ) |
21 |
|
efgredlemd.9 |
|- ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) ) |
22 |
|
efgredlemd.c |
|- ( ph -> C e. dom S ) |
23 |
|
efgredlemd.sc |
|- ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
24 |
1 2 3 4 5 6
|
efgsf |
|- S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W |
25 |
24
|
fdmi |
|- dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |
26 |
25
|
feq2i |
|- ( S : dom S --> W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W ) |
27 |
24 26
|
mpbir |
|- S : dom S --> W |
28 |
27
|
ffvelrni |
|- ( C e. dom S -> ( S ` C ) e. W ) |
29 |
22 28
|
syl |
|- ( ph -> ( S ` C ) e. W ) |
30 |
|
elfzuz |
|- ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) -> Q e. ( ZZ>= ` 0 ) ) |
31 |
15 30
|
syl |
|- ( ph -> Q e. ( ZZ>= ` 0 ) ) |
32 |
23
|
fveq2d |
|- ( ph -> ( # ` ( S ` C ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) ) |
33 |
|
fviss |
|- ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o ) |
34 |
1 33
|
eqsstri |
|- W C_ Word ( I X. 2o ) |
35 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
efgredlemf |
|- ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) ) |
36 |
35
|
simprd |
|- ( ph -> ( B ` L ) e. W ) |
37 |
34 36
|
sseldi |
|- ( ph -> ( B ` L ) e. Word ( I X. 2o ) ) |
38 |
|
pfxcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) ) |
39 |
37 38
|
syl |
|- ( ph -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) ) |
40 |
35
|
simpld |
|- ( ph -> ( A ` K ) e. W ) |
41 |
34 40
|
sseldi |
|- ( ph -> ( A ` K ) e. Word ( I X. 2o ) ) |
42 |
|
swrdcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) |
43 |
41 42
|
syl |
|- ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) |
44 |
|
ccatlen |
|- ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) ) |
45 |
39 43 44
|
syl2anc |
|- ( ph -> ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) ) |
46 |
|
pfxlen |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix Q ) ) = Q ) |
47 |
37 15 46
|
syl2anc |
|- ( ph -> ( # ` ( ( B ` L ) prefix Q ) ) = Q ) |
48 |
|
2nn0 |
|- 2 e. NN0 |
49 |
|
uzaddcl |
|- ( ( Q e. ( ZZ>= ` 0 ) /\ 2 e. NN0 ) -> ( Q + 2 ) e. ( ZZ>= ` 0 ) ) |
50 |
31 48 49
|
sylancl |
|- ( ph -> ( Q + 2 ) e. ( ZZ>= ` 0 ) ) |
51 |
|
elfzuz3 |
|- ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) ) |
52 |
14 51
|
syl |
|- ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) ) |
53 |
|
uztrn |
|- ( ( ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) ) |
54 |
52 21 53
|
syl2anc |
|- ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) ) |
55 |
|
elfzuzb |
|- ( ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) <-> ( ( Q + 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) ) ) |
56 |
50 54 55
|
sylanbrc |
|- ( ph -> ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) |
57 |
|
lencl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 ) |
58 |
41 57
|
syl |
|- ( ph -> ( # ` ( A ` K ) ) e. NN0 ) |
59 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
60 |
58 59
|
eleqtrdi |
|- ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) ) |
61 |
|
eluzfz2 |
|- ( ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) |
62 |
60 61
|
syl |
|- ( ph -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) |
63 |
|
swrdlen |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) |
64 |
41 56 62 63
|
syl3anc |
|- ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) |
65 |
47 64
|
oveq12d |
|- ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( Q + ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) ) |
66 |
|
elfzelz |
|- ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) -> Q e. ZZ ) |
67 |
15 66
|
syl |
|- ( ph -> Q e. ZZ ) |
68 |
67
|
zcnd |
|- ( ph -> Q e. CC ) |
69 |
58
|
nn0cnd |
|- ( ph -> ( # ` ( A ` K ) ) e. CC ) |
70 |
|
2z |
|- 2 e. ZZ |
71 |
|
zaddcl |
|- ( ( Q e. ZZ /\ 2 e. ZZ ) -> ( Q + 2 ) e. ZZ ) |
72 |
67 70 71
|
sylancl |
|- ( ph -> ( Q + 2 ) e. ZZ ) |
73 |
72
|
zcnd |
|- ( ph -> ( Q + 2 ) e. CC ) |
74 |
68 69 73
|
addsubassd |
|- ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( Q + ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) ) |
75 |
|
2cn |
|- 2 e. CC |
76 |
75
|
a1i |
|- ( ph -> 2 e. CC ) |
77 |
68 69 76
|
pnpcand |
|- ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( ( # ` ( A ` K ) ) - 2 ) ) |
78 |
65 74 77
|
3eqtr2d |
|- ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( A ` K ) ) - 2 ) ) |
79 |
32 45 78
|
3eqtrd |
|- ( ph -> ( # ` ( S ` C ) ) = ( ( # ` ( A ` K ) ) - 2 ) ) |
80 |
|
elfzelz |
|- ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ZZ ) |
81 |
14 80
|
syl |
|- ( ph -> P e. ZZ ) |
82 |
|
zsubcl |
|- ( ( P e. ZZ /\ 2 e. ZZ ) -> ( P - 2 ) e. ZZ ) |
83 |
81 70 82
|
sylancl |
|- ( ph -> ( P - 2 ) e. ZZ ) |
84 |
70
|
a1i |
|- ( ph -> 2 e. ZZ ) |
85 |
81
|
zcnd |
|- ( ph -> P e. CC ) |
86 |
|
npcan |
|- ( ( P e. CC /\ 2 e. CC ) -> ( ( P - 2 ) + 2 ) = P ) |
87 |
85 75 86
|
sylancl |
|- ( ph -> ( ( P - 2 ) + 2 ) = P ) |
88 |
87
|
fveq2d |
|- ( ph -> ( ZZ>= ` ( ( P - 2 ) + 2 ) ) = ( ZZ>= ` P ) ) |
89 |
52 88
|
eleqtrrd |
|- ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) ) |
90 |
|
eluzsub |
|- ( ( ( P - 2 ) e. ZZ /\ 2 e. ZZ /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) ) -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) ) |
91 |
83 84 89 90
|
syl3anc |
|- ( ph -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) ) |
92 |
79 91
|
eqeltrd |
|- ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) ) |
93 |
|
eluzsub |
|- ( ( Q e. ZZ /\ 2 e. ZZ /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( P - 2 ) e. ( ZZ>= ` Q ) ) |
94 |
67 84 21 93
|
syl3anc |
|- ( ph -> ( P - 2 ) e. ( ZZ>= ` Q ) ) |
95 |
|
uztrn |
|- ( ( ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) ) |
96 |
92 94 95
|
syl2anc |
|- ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) ) |
97 |
|
elfzuzb |
|- ( Q e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) ) ) |
98 |
31 96 97
|
sylanbrc |
|- ( ph -> Q e. ( 0 ... ( # ` ( S ` C ) ) ) ) |
99 |
1 2 3 4
|
efgtval |
|- ( ( ( S ` C ) e. W /\ Q e. ( 0 ... ( # ` ( S ` C ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( S ` C ) ) V ) = ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) ) |
100 |
29 98 17 99
|
syl3anc |
|- ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) ) |
101 |
|
pfxcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) ) |
102 |
41 101
|
syl |
|- ( ph -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) ) |
103 |
|
wrd0 |
|- (/) e. Word ( I X. 2o ) |
104 |
103
|
a1i |
|- ( ph -> (/) e. Word ( I X. 2o ) ) |
105 |
3
|
efgmf |
|- M : ( I X. 2o ) --> ( I X. 2o ) |
106 |
105
|
ffvelrni |
|- ( V e. ( I X. 2o ) -> ( M ` V ) e. ( I X. 2o ) ) |
107 |
17 106
|
syl |
|- ( ph -> ( M ` V ) e. ( I X. 2o ) ) |
108 |
17 107
|
s2cld |
|- ( ph -> <" V ( M ` V ) "> e. Word ( I X. 2o ) ) |
109 |
67
|
zred |
|- ( ph -> Q e. RR ) |
110 |
|
nn0addge1 |
|- ( ( Q e. RR /\ 2 e. NN0 ) -> Q <_ ( Q + 2 ) ) |
111 |
109 48 110
|
sylancl |
|- ( ph -> Q <_ ( Q + 2 ) ) |
112 |
|
eluz2 |
|- ( ( Q + 2 ) e. ( ZZ>= ` Q ) <-> ( Q e. ZZ /\ ( Q + 2 ) e. ZZ /\ Q <_ ( Q + 2 ) ) ) |
113 |
67 72 111 112
|
syl3anbrc |
|- ( ph -> ( Q + 2 ) e. ( ZZ>= ` Q ) ) |
114 |
|
uztrn |
|- ( ( P e. ( ZZ>= ` ( Q + 2 ) ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) -> P e. ( ZZ>= ` Q ) ) |
115 |
21 113 114
|
syl2anc |
|- ( ph -> P e. ( ZZ>= ` Q ) ) |
116 |
|
elfzuzb |
|- ( Q e. ( 0 ... P ) <-> ( Q e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` Q ) ) ) |
117 |
31 115 116
|
sylanbrc |
|- ( ph -> Q e. ( 0 ... P ) ) |
118 |
|
ccatpfx |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) = ( ( A ` K ) prefix P ) ) |
119 |
41 117 14 118
|
syl3anc |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) = ( ( A ` K ) prefix P ) ) |
120 |
119
|
oveq1d |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) |
121 |
|
pfxcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) ) |
122 |
41 121
|
syl |
|- ( ph -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) ) |
123 |
105
|
ffvelrni |
|- ( U e. ( I X. 2o ) -> ( M ` U ) e. ( I X. 2o ) ) |
124 |
16 123
|
syl |
|- ( ph -> ( M ` U ) e. ( I X. 2o ) ) |
125 |
16 124
|
s2cld |
|- ( ph -> <" U ( M ` U ) "> e. Word ( I X. 2o ) ) |
126 |
|
swrdcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) |
127 |
41 126
|
syl |
|- ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) |
128 |
|
ccatass |
|- ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) |
129 |
122 125 127 128
|
syl3anc |
|- ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) |
130 |
1 2 3 4
|
efgtval |
|- ( ( ( A ` K ) e. W /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ U e. ( I X. 2o ) ) -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) ) |
131 |
40 14 16 130
|
syl3anc |
|- ( ph -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) ) |
132 |
|
splval |
|- ( ( ( A ` K ) e. W /\ ( P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) ) ) -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) |
133 |
40 14 14 125 132
|
syl13anc |
|- ( ph -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) |
134 |
18 131 133
|
3eqtrd |
|- ( ph -> ( S ` A ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) |
135 |
1 2 3 4
|
efgtval |
|- ( ( ( B ` L ) e. W /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) ) |
136 |
36 15 17 135
|
syl3anc |
|- ( ph -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) ) |
137 |
|
splval |
|- ( ( ( B ` L ) e. W /\ ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) ) ) -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
138 |
36 15 15 108 137
|
syl13anc |
|- ( ph -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
139 |
19 136 138
|
3eqtrd |
|- ( ph -> ( S ` B ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
140 |
10 134 139
|
3eqtr3d |
|- ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
141 |
120 129 140
|
3eqtr2d |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
142 |
|
swrdcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) ) |
143 |
41 142
|
syl |
|- ( ph -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) ) |
144 |
|
ccatcl |
|- ( ( <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) |
145 |
125 127 144
|
syl2anc |
|- ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) |
146 |
|
ccatass |
|- ( ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) ) |
147 |
102 143 145 146
|
syl3anc |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) ) |
148 |
|
swrdcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
149 |
37 148
|
syl |
|- ( ph -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
150 |
|
ccatass |
|- ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
151 |
39 108 149 150
|
syl3anc |
|- ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
152 |
141 147 151
|
3eqtr3d |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
153 |
|
ccatcl |
|- ( ( ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) |
154 |
143 145 153
|
syl2anc |
|- ( ph -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) |
155 |
|
ccatcl |
|- ( ( <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) ) |
156 |
108 149 155
|
syl2anc |
|- ( ph -> ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) ) |
157 |
|
uztrn |
|- ( ( ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` Q ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) ) |
158 |
52 115 157
|
syl2anc |
|- ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) ) |
159 |
|
elfzuzb |
|- ( Q e. ( 0 ... ( # ` ( A ` K ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) ) ) |
160 |
31 158 159
|
sylanbrc |
|- ( ph -> Q e. ( 0 ... ( # ` ( A ` K ) ) ) ) |
161 |
|
pfxlen |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) prefix Q ) ) = Q ) |
162 |
41 160 161
|
syl2anc |
|- ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = Q ) |
163 |
162 47
|
eqtr4d |
|- ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = ( # ` ( ( B ` L ) prefix Q ) ) ) |
164 |
|
ccatopth |
|- ( ( ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) prefix Q ) ) = ( # ` ( ( B ` L ) prefix Q ) ) ) -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) <-> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) ) |
165 |
102 154 39 156 163 164
|
syl221anc |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) <-> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) ) |
166 |
152 165
|
mpbid |
|- ( ph -> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
167 |
166
|
simpld |
|- ( ph -> ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) ) |
168 |
167
|
oveq1d |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
169 |
|
ccatrid |
|- ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) ) |
170 |
102 169
|
syl |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) ) |
171 |
170
|
oveq1d |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
172 |
168 171 23
|
3eqtr4rd |
|- ( ph -> ( S ` C ) = ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
173 |
162
|
eqcomd |
|- ( ph -> Q = ( # ` ( ( A ` K ) prefix Q ) ) ) |
174 |
|
hash0 |
|- ( # ` (/) ) = 0 |
175 |
174
|
oveq2i |
|- ( Q + ( # ` (/) ) ) = ( Q + 0 ) |
176 |
68
|
addid1d |
|- ( ph -> ( Q + 0 ) = Q ) |
177 |
175 176
|
syl5req |
|- ( ph -> Q = ( Q + ( # ` (/) ) ) ) |
178 |
102 104 43 108 172 173 177
|
splval2 |
|- ( ph -> ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
179 |
|
elfzuzb |
|- ( Q e. ( 0 ... ( Q + 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) ) |
180 |
31 113 179
|
sylanbrc |
|- ( ph -> Q e. ( 0 ... ( Q + 2 ) ) ) |
181 |
|
elfzuzb |
|- ( ( Q + 2 ) e. ( 0 ... P ) <-> ( ( Q + 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) ) |
182 |
50 21 181
|
sylanbrc |
|- ( ph -> ( Q + 2 ) e. ( 0 ... P ) ) |
183 |
|
ccatswrd |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) ) -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( ( A ` K ) substr <. Q , P >. ) ) |
184 |
41 180 182 14 183
|
syl13anc |
|- ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( ( A ` K ) substr <. Q , P >. ) ) |
185 |
184
|
oveq1d |
|- ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) |
186 |
|
swrdcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) ) |
187 |
41 186
|
syl |
|- ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) ) |
188 |
|
swrdcl |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) ) |
189 |
41 188
|
syl |
|- ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) ) |
190 |
|
ccatass |
|- ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) ) |
191 |
187 189 145 190
|
syl3anc |
|- ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) ) |
192 |
166
|
simprd |
|- ( ph -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
193 |
185 191 192
|
3eqtr3d |
|- ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
194 |
|
ccatcl |
|- ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) |
195 |
189 145 194
|
syl2anc |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) |
196 |
|
swrdlen |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( Q + 2 ) - Q ) ) |
197 |
41 180 56 196
|
syl3anc |
|- ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( Q + 2 ) - Q ) ) |
198 |
|
pncan2 |
|- ( ( Q e. CC /\ 2 e. CC ) -> ( ( Q + 2 ) - Q ) = 2 ) |
199 |
68 75 198
|
sylancl |
|- ( ph -> ( ( Q + 2 ) - Q ) = 2 ) |
200 |
197 199
|
eqtrd |
|- ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = 2 ) |
201 |
|
s2len |
|- ( # ` <" V ( M ` V ) "> ) = 2 |
202 |
200 201
|
eqtr4di |
|- ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( # ` <" V ( M ` V ) "> ) ) |
203 |
|
ccatopth |
|- ( ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) /\ ( <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( # ` <" V ( M ` V ) "> ) ) -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
204 |
187 195 108 149 202 203
|
syl221anc |
|- ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) |
205 |
193 204
|
mpbid |
|- ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) |
206 |
205
|
simpld |
|- ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> ) |
207 |
206
|
oveq2d |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ) |
208 |
|
ccatpfx |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( A ` K ) prefix ( Q + 2 ) ) ) |
209 |
41 180 56 208
|
syl3anc |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( A ` K ) prefix ( Q + 2 ) ) ) |
210 |
207 209
|
eqtr3d |
|- ( ph -> ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) = ( ( A ` K ) prefix ( Q + 2 ) ) ) |
211 |
210
|
oveq1d |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) |
212 |
|
ccatpfx |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) ) |
213 |
41 56 62 212
|
syl3anc |
|- ( ph -> ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) ) |
214 |
|
pfxid |
|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) ) |
215 |
41 214
|
syl |
|- ( ph -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) ) |
216 |
211 213 215
|
3eqtrd |
|- ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( A ` K ) ) |
217 |
100 178 216
|
3eqtrd |
|- ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( A ` K ) ) |
218 |
1 2 3 4
|
efgtf |
|- ( ( S ` C ) e. W -> ( ( T ` ( S ` C ) ) = ( a e. ( 0 ... ( # ` ( S ` C ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` C ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W ) ) |
219 |
29 218
|
syl |
|- ( ph -> ( ( T ` ( S ` C ) ) = ( a e. ( 0 ... ( # ` ( S ` C ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` C ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W ) ) |
220 |
219
|
simprd |
|- ( ph -> ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W ) |
221 |
220
|
ffnd |
|- ( ph -> ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) ) |
222 |
|
fnovrn |
|- ( ( ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) /\ Q e. ( 0 ... ( # ` ( S ` C ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( S ` C ) ) V ) e. ran ( T ` ( S ` C ) ) ) |
223 |
221 98 17 222
|
syl3anc |
|- ( ph -> ( Q ( T ` ( S ` C ) ) V ) e. ran ( T ` ( S ` C ) ) ) |
224 |
217 223
|
eqeltrrd |
|- ( ph -> ( A ` K ) e. ran ( T ` ( S ` C ) ) ) |
225 |
|
uztrn |
|- ( ( ( P - 2 ) e. ( ZZ>= ` Q ) /\ Q e. ( ZZ>= ` 0 ) ) -> ( P - 2 ) e. ( ZZ>= ` 0 ) ) |
226 |
94 31 225
|
syl2anc |
|- ( ph -> ( P - 2 ) e. ( ZZ>= ` 0 ) ) |
227 |
|
elfzuzb |
|- ( ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) ) ) |
228 |
226 92 227
|
sylanbrc |
|- ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) ) |
229 |
1 2 3 4
|
efgtval |
|- ( ( ( S ` C ) e. W /\ ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) /\ U e. ( I X. 2o ) ) -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) ) |
230 |
29 228 16 229
|
syl3anc |
|- ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) ) |
231 |
|
pfxcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) ) |
232 |
37 231
|
syl |
|- ( ph -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) ) |
233 |
|
swrdcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
234 |
37 233
|
syl |
|- ( ph -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
235 |
|
ccatswrd |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) ) -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) |
236 |
41 182 14 62 235
|
syl13anc |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) |
237 |
205
|
simprd |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) |
238 |
|
elfzuzb |
|- ( Q e. ( 0 ... ( P - 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) ) |
239 |
31 94 238
|
sylanbrc |
|- ( ph -> Q e. ( 0 ... ( P - 2 ) ) ) |
240 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
|
efgredlemg |
|- ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) ) |
241 |
240 52
|
eqeltrrd |
|- ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) ) |
242 |
|
0le2 |
|- 0 <_ 2 |
243 |
242
|
a1i |
|- ( ph -> 0 <_ 2 ) |
244 |
81
|
zred |
|- ( ph -> P e. RR ) |
245 |
|
2re |
|- 2 e. RR |
246 |
|
subge02 |
|- ( ( P e. RR /\ 2 e. RR ) -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) ) |
247 |
244 245 246
|
sylancl |
|- ( ph -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) ) |
248 |
243 247
|
mpbid |
|- ( ph -> ( P - 2 ) <_ P ) |
249 |
|
eluz2 |
|- ( P e. ( ZZ>= ` ( P - 2 ) ) <-> ( ( P - 2 ) e. ZZ /\ P e. ZZ /\ ( P - 2 ) <_ P ) ) |
250 |
83 81 248 249
|
syl3anbrc |
|- ( ph -> P e. ( ZZ>= ` ( P - 2 ) ) ) |
251 |
|
uztrn |
|- ( ( ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) ) |
252 |
241 250 251
|
syl2anc |
|- ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) ) |
253 |
|
elfzuzb |
|- ( ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) ) ) |
254 |
226 252 253
|
sylanbrc |
|- ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) |
255 |
|
lencl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 ) |
256 |
37 255
|
syl |
|- ( ph -> ( # ` ( B ` L ) ) e. NN0 ) |
257 |
256 59
|
eleqtrdi |
|- ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) ) |
258 |
|
eluzfz2 |
|- ( ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) |
259 |
257 258
|
syl |
|- ( ph -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) |
260 |
|
ccatswrd |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) ) -> ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) |
261 |
37 239 254 259 260
|
syl13anc |
|- ( ph -> ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) |
262 |
237 261
|
eqtr4d |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) |
263 |
|
swrdcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) ) |
264 |
37 263
|
syl |
|- ( ph -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) ) |
265 |
|
swrdcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
266 |
37 265
|
syl |
|- ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) |
267 |
|
swrdlen |
|- ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( P - ( Q + 2 ) ) ) |
268 |
41 182 14 267
|
syl3anc |
|- ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( P - ( Q + 2 ) ) ) |
269 |
|
swrdlen |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( P - 2 ) - Q ) ) |
270 |
37 239 254 269
|
syl3anc |
|- ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( P - 2 ) - Q ) ) |
271 |
85 68 76
|
sub32d |
|- ( ph -> ( ( P - Q ) - 2 ) = ( ( P - 2 ) - Q ) ) |
272 |
85 68 76
|
subsub4d |
|- ( ph -> ( ( P - Q ) - 2 ) = ( P - ( Q + 2 ) ) ) |
273 |
270 271 272
|
3eqtr2d |
|- ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( P - ( Q + 2 ) ) ) |
274 |
268 273
|
eqtr4d |
|- ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ) |
275 |
|
ccatopth |
|- ( ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ) -> ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) ) |
276 |
189 145 264 266 274 275
|
syl221anc |
|- ( ph -> ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) ) |
277 |
262 276
|
mpbid |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) |
278 |
277
|
simpld |
|- ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) |
279 |
277
|
simprd |
|- ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) |
280 |
|
elfzuzb |
|- ( ( P - 2 ) e. ( 0 ... P ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) ) |
281 |
226 250 280
|
sylanbrc |
|- ( ph -> ( P - 2 ) e. ( 0 ... P ) ) |
282 |
|
elfzuz |
|- ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ( ZZ>= ` 0 ) ) |
283 |
14 282
|
syl |
|- ( ph -> P e. ( ZZ>= ` 0 ) ) |
284 |
|
elfzuzb |
|- ( P e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( P e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) ) ) |
285 |
283 241 284
|
sylanbrc |
|- ( ph -> P e. ( 0 ... ( # ` ( B ` L ) ) ) ) |
286 |
|
ccatswrd |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) ) -> ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) |
287 |
37 281 285 259 286
|
syl13anc |
|- ( ph -> ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) |
288 |
279 287
|
eqtr4d |
|- ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
289 |
|
swrdcl |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) ) |
290 |
37 289
|
syl |
|- ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) ) |
291 |
|
s2len |
|- ( # ` <" U ( M ` U ) "> ) = 2 |
292 |
|
swrdlen |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( P - ( P - 2 ) ) ) |
293 |
37 281 285 292
|
syl3anc |
|- ( ph -> ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( P - ( P - 2 ) ) ) |
294 |
|
nncan |
|- ( ( P e. CC /\ 2 e. CC ) -> ( P - ( P - 2 ) ) = 2 ) |
295 |
85 75 294
|
sylancl |
|- ( ph -> ( P - ( P - 2 ) ) = 2 ) |
296 |
293 295
|
eqtr2d |
|- ( ph -> 2 = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) ) |
297 |
291 296
|
syl5eq |
|- ( ph -> ( # ` <" U ( M ` U ) "> ) = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) ) |
298 |
|
ccatopth |
|- ( ( ( <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` <" U ( M ` U ) "> ) = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) ) -> ( ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) <-> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) ) |
299 |
125 127 290 234 297 298
|
syl221anc |
|- ( ph -> ( ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) <-> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) ) |
300 |
288 299
|
mpbid |
|- ( ph -> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
301 |
300
|
simprd |
|- ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) |
302 |
278 301
|
oveq12d |
|- ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
303 |
236 302
|
eqtr3d |
|- ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
304 |
303
|
oveq2d |
|- ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) ) |
305 |
|
ccatass |
|- ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) ) |
306 |
39 264 234 305
|
syl3anc |
|- ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) ) |
307 |
304 306
|
eqtr4d |
|- ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
308 |
|
ccatpfx |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( B ` L ) prefix ( P - 2 ) ) ) |
309 |
37 239 254 308
|
syl3anc |
|- ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( B ` L ) prefix ( P - 2 ) ) ) |
310 |
309
|
oveq1d |
|- ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
311 |
23 307 310
|
3eqtrd |
|- ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
312 |
|
ccatrid |
|- ( ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) ) |
313 |
232 312
|
syl |
|- ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) ) |
314 |
313
|
oveq1d |
|- ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
315 |
311 314
|
eqtr4d |
|- ( ph -> ( S ` C ) = ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
316 |
|
pfxlen |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) ) |
317 |
37 254 316
|
syl2anc |
|- ( ph -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) ) |
318 |
317
|
eqcomd |
|- ( ph -> ( P - 2 ) = ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) ) |
319 |
174
|
oveq2i |
|- ( ( P - 2 ) + ( # ` (/) ) ) = ( ( P - 2 ) + 0 ) |
320 |
83
|
zcnd |
|- ( ph -> ( P - 2 ) e. CC ) |
321 |
320
|
addid1d |
|- ( ph -> ( ( P - 2 ) + 0 ) = ( P - 2 ) ) |
322 |
319 321
|
syl5req |
|- ( ph -> ( P - 2 ) = ( ( P - 2 ) + ( # ` (/) ) ) ) |
323 |
232 104 234 125 315 318 322
|
splval2 |
|- ( ph -> ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) = ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
324 |
300
|
simpld |
|- ( ph -> <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) |
325 |
324
|
oveq2d |
|- ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) ) |
326 |
|
ccatpfx |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( ( B ` L ) prefix P ) ) |
327 |
37 281 285 326
|
syl3anc |
|- ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( ( B ` L ) prefix P ) ) |
328 |
325 327
|
eqtrd |
|- ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( B ` L ) prefix P ) ) |
329 |
328
|
oveq1d |
|- ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) |
330 |
|
ccatpfx |
|- ( ( ( B ` L ) e. Word ( I X. 2o ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) ) |
331 |
37 285 259 330
|
syl3anc |
|- ( ph -> ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) ) |
332 |
|
pfxid |
|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) ) |
333 |
37 332
|
syl |
|- ( ph -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) ) |
334 |
329 331 333
|
3eqtrd |
|- ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( B ` L ) ) |
335 |
230 323 334
|
3eqtrd |
|- ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( B ` L ) ) |
336 |
|
fnovrn |
|- ( ( ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) /\ U e. ( I X. 2o ) ) -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) e. ran ( T ` ( S ` C ) ) ) |
337 |
221 228 16 336
|
syl3anc |
|- ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) e. ran ( T ` ( S ` C ) ) ) |
338 |
335 337
|
eqeltrrd |
|- ( ph -> ( B ` L ) e. ran ( T ` ( S ` C ) ) ) |
339 |
224 338
|
jca |
|- ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) ) |