| 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 |
|
ldualvs.a |
|- ( ph -> A e. V ) |
| 12 |
1 2 3 4 5 6 7 8 9 10
|
ldualvs |
|- ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) ) |
| 13 |
12
|
fveq1d |
|- ( ph -> ( ( X .xb G ) ` A ) = ( ( G oF .X. ( V X. { X } ) ) ` A ) ) |
| 14 |
2
|
fvexi |
|- V e. _V |
| 15 |
14
|
a1i |
|- ( ph -> V e. _V ) |
| 16 |
3 4 2 1
|
lflf |
|- ( ( W e. Y /\ G e. F ) -> G : V --> K ) |
| 17 |
8 10 16
|
syl2anc |
|- ( ph -> G : V --> K ) |
| 18 |
17
|
ffnd |
|- ( ph -> G Fn V ) |
| 19 |
|
eqidd |
|- ( ( ph /\ A e. V ) -> ( G ` A ) = ( G ` A ) ) |
| 20 |
15 9 18 19
|
ofc2 |
|- ( ( ph /\ A e. V ) -> ( ( G oF .X. ( V X. { X } ) ) ` A ) = ( ( G ` A ) .X. X ) ) |
| 21 |
11 20
|
mpdan |
|- ( ph -> ( ( G oF .X. ( V X. { X } ) ) ` A ) = ( ( G ` A ) .X. X ) ) |
| 22 |
13 21
|
eqtrd |
|- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .X. X ) ) |