| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lsatel.o |
|- .0. = ( 0g ` W ) |
| 2 |
|
lsatel.n |
|- N = ( LSpan ` W ) |
| 3 |
|
lsatel.a |
|- A = ( LSAtoms ` W ) |
| 4 |
|
lsatel.w |
|- ( ph -> W e. LVec ) |
| 5 |
|
lsatel.u |
|- ( ph -> U e. A ) |
| 6 |
|
lsatel.x |
|- ( ph -> X e. U ) |
| 7 |
|
lsatel.e |
|- ( ph -> X =/= .0. ) |
| 8 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
| 9 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
| 10 |
4 9
|
syl |
|- ( ph -> W e. LMod ) |
| 11 |
8 3 10 5
|
lsatlssel |
|- ( ph -> U e. ( LSubSp ` W ) ) |
| 12 |
8 2 10 11 6
|
ellspsn5 |
|- ( ph -> ( N ` { X } ) C_ U ) |
| 13 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 14 |
13 8
|
lssel |
|- ( ( U e. ( LSubSp ` W ) /\ X e. U ) -> X e. ( Base ` W ) ) |
| 15 |
11 6 14
|
syl2anc |
|- ( ph -> X e. ( Base ` W ) ) |
| 16 |
13 2 1 3
|
lsatlspsn2 |
|- ( ( W e. LMod /\ X e. ( Base ` W ) /\ X =/= .0. ) -> ( N ` { X } ) e. A ) |
| 17 |
10 15 7 16
|
syl3anc |
|- ( ph -> ( N ` { X } ) e. A ) |
| 18 |
3 4 17 5
|
lsatcmp |
|- ( ph -> ( ( N ` { X } ) C_ U <-> ( N ` { X } ) = U ) ) |
| 19 |
12 18
|
mpbid |
|- ( ph -> ( N ` { X } ) = U ) |
| 20 |
19
|
eqcomd |
|- ( ph -> U = ( N ` { X } ) ) |