Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
0ex |
|- (/) e. _V |
4 |
3
|
prid1 |
|- (/) e. { (/) , 1o } |
5 |
|
df2o3 |
|- 2o = { (/) , 1o } |
6 |
4 5
|
eleqtrri |
|- (/) e. 2o |
7 |
1 2
|
efgi |
|- ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ (/) e. 2o ) ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. ) ) |
8 |
6 7
|
mpanr2 |
|- ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. ) ) |
9 |
8
|
3impa |
|- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. ) ) |
10 |
|
tru |
|- T. |
11 |
|
eqidd |
|- ( T. -> <. J , (/) >. = <. J , (/) >. ) |
12 |
|
dif0 |
|- ( 1o \ (/) ) = 1o |
13 |
12
|
opeq2i |
|- <. J , ( 1o \ (/) ) >. = <. J , 1o >. |
14 |
13
|
a1i |
|- ( T. -> <. J , ( 1o \ (/) ) >. = <. J , 1o >. ) |
15 |
11 14
|
s2eqd |
|- ( T. -> <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> = <" <. J , (/) >. <. J , 1o >. "> ) |
16 |
|
oteq3 |
|- ( <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> = <" <. J , (/) >. <. J , 1o >. "> -> <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. = <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) |
17 |
10 15 16
|
mp2b |
|- <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. = <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. |
18 |
17
|
oveq2i |
|- ( A splice <. N , N , <" <. J , (/) >. <. J , ( 1o \ (/) ) >. "> >. ) = ( A splice <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) |
19 |
9 18
|
breqtrdi |
|- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) ) |