| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lspsn0.z |
|- .0. = ( 0g ` W ) |
| 2 |
|
lspsn0.n |
|- N = ( LSpan ` W ) |
| 3 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
| 4 |
1 3
|
lsssn0 |
|- ( W e. LMod -> { .0. } e. ( LSubSp ` W ) ) |
| 5 |
|
0ss |
|- (/) C_ { .0. } |
| 6 |
3 2
|
lspssp |
|- ( ( W e. LMod /\ { .0. } e. ( LSubSp ` W ) /\ (/) C_ { .0. } ) -> ( N ` (/) ) C_ { .0. } ) |
| 7 |
5 6
|
mp3an3 |
|- ( ( W e. LMod /\ { .0. } e. ( LSubSp ` W ) ) -> ( N ` (/) ) C_ { .0. } ) |
| 8 |
4 7
|
mpdan |
|- ( W e. LMod -> ( N ` (/) ) C_ { .0. } ) |
| 9 |
|
0ss |
|- (/) C_ ( Base ` W ) |
| 10 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 11 |
10 3 2
|
lspcl |
|- ( ( W e. LMod /\ (/) C_ ( Base ` W ) ) -> ( N ` (/) ) e. ( LSubSp ` W ) ) |
| 12 |
9 11
|
mpan2 |
|- ( W e. LMod -> ( N ` (/) ) e. ( LSubSp ` W ) ) |
| 13 |
1 3
|
lss0ss |
|- ( ( W e. LMod /\ ( N ` (/) ) e. ( LSubSp ` W ) ) -> { .0. } C_ ( N ` (/) ) ) |
| 14 |
12 13
|
mpdan |
|- ( W e. LMod -> { .0. } C_ ( N ` (/) ) ) |
| 15 |
8 14
|
eqssd |
|- ( W e. LMod -> ( N ` (/) ) = { .0. } ) |