| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ldualfvs.f |
|- F = ( LFnl ` W ) |
| 2 |
|
ldualfvs.v |
|- V = ( Base ` W ) |
| 3 |
|
ldualfvs.r |
|- R = ( Scalar ` W ) |
| 4 |
|
ldualfvs.k |
|- K = ( Base ` R ) |
| 5 |
|
ldualfvs.t |
|- .X. = ( .r ` R ) |
| 6 |
|
ldualfvs.d |
|- D = ( LDual ` W ) |
| 7 |
|
ldualfvs.s |
|- .xb = ( .s ` D ) |
| 8 |
|
ldualfvs.w |
|- ( ph -> W e. Y ) |
| 9 |
|
ldualvs.x |
|- ( ph -> X e. K ) |
| 10 |
|
ldualvs.g |
|- ( ph -> G e. F ) |
| 11 |
|
eqid |
|- ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) |
| 12 |
1 2 3 4 5 6 7 8 11
|
ldualfvs |
|- ( ph -> .xb = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) ) |
| 13 |
12
|
oveqd |
|- ( ph -> ( X .xb G ) = ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) ) |
| 14 |
|
sneq |
|- ( k = X -> { k } = { X } ) |
| 15 |
14
|
xpeq2d |
|- ( k = X -> ( V X. { k } ) = ( V X. { X } ) ) |
| 16 |
15
|
oveq2d |
|- ( k = X -> ( f oF .X. ( V X. { k } ) ) = ( f oF .X. ( V X. { X } ) ) ) |
| 17 |
|
oveq1 |
|- ( f = G -> ( f oF .X. ( V X. { X } ) ) = ( G oF .X. ( V X. { X } ) ) ) |
| 18 |
|
ovex |
|- ( G oF .X. ( V X. { X } ) ) e. _V |
| 19 |
16 17 11 18
|
ovmpo |
|- ( ( X e. K /\ G e. F ) -> ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) = ( G oF .X. ( V X. { X } ) ) ) |
| 20 |
9 10 19
|
syl2anc |
|- ( ph -> ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) = ( G oF .X. ( V X. { X } ) ) ) |
| 21 |
13 20
|
eqtrd |
|- ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) ) |