| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lduallkr3.h |
|- H = ( LSHyp ` W ) |
| 2 |
|
lduallkr3.f |
|- F = ( LFnl ` W ) |
| 3 |
|
lduallkr3.k |
|- K = ( LKer ` W ) |
| 4 |
|
lduallkr3.d |
|- D = ( LDual ` W ) |
| 5 |
|
lduallkr3.o |
|- .0. = ( 0g ` D ) |
| 6 |
|
lduallkr3.w |
|- ( ph -> W e. LVec ) |
| 7 |
|
lduallkr3.g |
|- ( ph -> G e. F ) |
| 8 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 9 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 10 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
| 11 |
8 9 10 1 2 3 6 7
|
lkrshp3 |
|- ( ph -> ( ( K ` G ) e. H <-> G =/= ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) ) |
| 12 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
| 13 |
6 12
|
syl |
|- ( ph -> W e. LMod ) |
| 14 |
8 9 10 4 5 13
|
ldual0v |
|- ( ph -> .0. = ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) |
| 15 |
14
|
neeq2d |
|- ( ph -> ( G =/= .0. <-> G =/= ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) ) |
| 16 |
11 15
|
bitr4d |
|- ( ph -> ( ( K ` G ) e. H <-> G =/= .0. ) ) |