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 |
1 2 3 4
|
efgtf |
|- ( X e. W -> ( ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` X ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W ) ) |
6 |
5
|
simpld |
|- ( X e. W -> ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) ) |
7 |
6
|
oveqd |
|- ( X e. W -> ( N ( T ` X ) A ) = ( N ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) A ) ) |
8 |
|
oteq1 |
|- ( a = N -> <. a , a , <" b ( M ` b ) "> >. = <. N , a , <" b ( M ` b ) "> >. ) |
9 |
|
oteq2 |
|- ( a = N -> <. N , a , <" b ( M ` b ) "> >. = <. N , N , <" b ( M ` b ) "> >. ) |
10 |
8 9
|
eqtrd |
|- ( a = N -> <. a , a , <" b ( M ` b ) "> >. = <. N , N , <" b ( M ` b ) "> >. ) |
11 |
10
|
oveq2d |
|- ( a = N -> ( X splice <. a , a , <" b ( M ` b ) "> >. ) = ( X splice <. N , N , <" b ( M ` b ) "> >. ) ) |
12 |
|
id |
|- ( b = A -> b = A ) |
13 |
|
fveq2 |
|- ( b = A -> ( M ` b ) = ( M ` A ) ) |
14 |
12 13
|
s2eqd |
|- ( b = A -> <" b ( M ` b ) "> = <" A ( M ` A ) "> ) |
15 |
14
|
oteq3d |
|- ( b = A -> <. N , N , <" b ( M ` b ) "> >. = <. N , N , <" A ( M ` A ) "> >. ) |
16 |
15
|
oveq2d |
|- ( b = A -> ( X splice <. N , N , <" b ( M ` b ) "> >. ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) ) |
17 |
|
eqid |
|- ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) |
18 |
|
ovex |
|- ( X splice <. N , N , <" A ( M ` A ) "> >. ) e. _V |
19 |
11 16 17 18
|
ovmpo |
|- ( ( N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) ) |
20 |
7 19
|
sylan9eq |
|- ( ( X e. W /\ ( N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) ) |
21 |
20
|
3impb |
|- ( ( X e. W /\ N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) ) |