| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ldualv0cl.f |
|- F = ( LFnl ` W ) |
| 2 |
|
ldualv0cl.d |
|- D = ( LDual ` W ) |
| 3 |
|
ldualv0cl.o |
|- .0. = ( 0g ` D ) |
| 4 |
|
ldualv0cl.w |
|- ( ph -> W e. LMod ) |
| 5 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 6 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 7 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
| 8 |
5 6 7 2 3 4
|
ldual0v |
|- ( ph -> .0. = ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) |
| 9 |
6 7 5 1
|
lfl0f |
|- ( W e. LMod -> ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) e. F ) |
| 10 |
4 9
|
syl |
|- ( ph -> ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) e. F ) |
| 11 |
8 10
|
eqeltrd |
|- ( ph -> .0. e. F ) |