| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cvsdiv.f |
|- F = ( Scalar ` W ) |
| 2 |
|
cvsdiv.k |
|- K = ( Base ` F ) |
| 3 |
|
id |
|- ( W e. CVec -> W e. CVec ) |
| 4 |
3
|
cvsclm |
|- ( W e. CVec -> W e. CMod ) |
| 5 |
1
|
clm0 |
|- ( W e. CMod -> 0 = ( 0g ` F ) ) |
| 6 |
4 5
|
syl |
|- ( W e. CVec -> 0 = ( 0g ` F ) ) |
| 7 |
6
|
sneqd |
|- ( W e. CVec -> { 0 } = { ( 0g ` F ) } ) |
| 8 |
7
|
difeq2d |
|- ( W e. CVec -> ( K \ { 0 } ) = ( K \ { ( 0g ` F ) } ) ) |
| 9 |
3
|
cvslvec |
|- ( W e. CVec -> W e. LVec ) |
| 10 |
1
|
lvecdrng |
|- ( W e. LVec -> F e. DivRing ) |
| 11 |
|
eqid |
|- ( Unit ` F ) = ( Unit ` F ) |
| 12 |
|
eqid |
|- ( 0g ` F ) = ( 0g ` F ) |
| 13 |
2 11 12
|
isdrng |
|- ( F e. DivRing <-> ( F e. Ring /\ ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) ) ) |
| 14 |
13
|
simprbi |
|- ( F e. DivRing -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) ) |
| 15 |
9 10 14
|
3syl |
|- ( W e. CVec -> ( Unit ` F ) = ( K \ { ( 0g ` F ) } ) ) |
| 16 |
8 15
|
eqtr4d |
|- ( W e. CVec -> ( K \ { 0 } ) = ( Unit ` F ) ) |