Step |
Hyp |
Ref |
Expression |
1 |
|
lsator0sp.v |
|- V = ( Base ` W ) |
2 |
|
lsator0sp.n |
|- N = ( LSpan ` W ) |
3 |
|
lsator0sp.o |
|- .0. = ( 0g ` W ) |
4 |
|
lsator0sp.a |
|- A = ( LSAtoms ` W ) |
5 |
|
isator0sp.w |
|- ( ph -> W e. LMod ) |
6 |
|
isator0sp.x |
|- ( ph -> X e. V ) |
7 |
1 2 3 4 5 6
|
lsatspn0 |
|- ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) ) |
8 |
7
|
biimprd |
|- ( ph -> ( X =/= .0. -> ( N ` { X } ) e. A ) ) |
9 |
8
|
necon1bd |
|- ( ph -> ( -. ( N ` { X } ) e. A -> X = .0. ) ) |
10 |
1 3 2
|
lspsneq0 |
|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) ) |
11 |
5 6 10
|
syl2anc |
|- ( ph -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) ) |
12 |
9 11
|
sylibrd |
|- ( ph -> ( -. ( N ` { X } ) e. A -> ( N ` { X } ) = { .0. } ) ) |
13 |
12
|
orrd |
|- ( ph -> ( ( N ` { X } ) e. A \/ ( N ` { X } ) = { .0. } ) ) |