| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lspsncmp.v |
|- V = ( Base ` W ) |
| 2 |
|
lspsncmp.o |
|- .0. = ( 0g ` W ) |
| 3 |
|
lspsncmp.n |
|- N = ( LSpan ` W ) |
| 4 |
|
lspsncmp.w |
|- ( ph -> W e. LVec ) |
| 5 |
|
lspsncmp.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
| 6 |
|
lspsncmp.y |
|- ( ph -> Y e. V ) |
| 7 |
4
|
adantr |
|- ( ( ph /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> W e. LVec ) |
| 8 |
6
|
adantr |
|- ( ( ph /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> Y e. V ) |
| 9 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
| 10 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
| 11 |
4 10
|
syl |
|- ( ph -> W e. LMod ) |
| 12 |
1 9 3
|
lspsncl |
|- ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) ) |
| 13 |
11 6 12
|
syl2anc |
|- ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) ) |
| 14 |
5
|
eldifad |
|- ( ph -> X e. V ) |
| 15 |
1 9 3 11 13 14
|
ellspsn5b |
|- ( ph -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) ) |
| 16 |
15
|
biimpar |
|- ( ( ph /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> X e. ( N ` { Y } ) ) |
| 17 |
|
eldifsni |
|- ( X e. ( V \ { .0. } ) -> X =/= .0. ) |
| 18 |
5 17
|
syl |
|- ( ph -> X =/= .0. ) |
| 19 |
18
|
adantr |
|- ( ( ph /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> X =/= .0. ) |
| 20 |
1 2 3 7 8 16 19
|
lspsneleq |
|- ( ( ph /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> ( N ` { X } ) = ( N ` { Y } ) ) |
| 21 |
20
|
ex |
|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) -> ( N ` { X } ) = ( N ` { Y } ) ) ) |
| 22 |
|
eqimss |
|- ( ( N ` { X } ) = ( N ` { Y } ) -> ( N ` { X } ) C_ ( N ` { Y } ) ) |
| 23 |
21 22
|
impbid1 |
|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> ( N ` { X } ) = ( N ` { Y } ) ) ) |