Step |
Hyp |
Ref |
Expression |
1 |
|
lsatssn0.o |
|- .0. = ( 0g ` W ) |
2 |
|
lsatssn0.a |
|- A = ( LSAtoms ` W ) |
3 |
|
lsatssn0.w |
|- ( ph -> W e. LMod ) |
4 |
|
lsatssn0.q |
|- ( ph -> Q e. A ) |
5 |
|
lsatssn0.u |
|- ( ph -> Q C_ U ) |
6 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
7 |
6 2 3 4
|
lsatlssel |
|- ( ph -> Q e. ( LSubSp ` W ) ) |
8 |
1 6
|
lss0ss |
|- ( ( W e. LMod /\ Q e. ( LSubSp ` W ) ) -> { .0. } C_ Q ) |
9 |
3 7 8
|
syl2anc |
|- ( ph -> { .0. } C_ Q ) |
10 |
1 2 3 4
|
lsatn0 |
|- ( ph -> Q =/= { .0. } ) |
11 |
10
|
necomd |
|- ( ph -> { .0. } =/= Q ) |
12 |
|
df-pss |
|- ( { .0. } C. Q <-> ( { .0. } C_ Q /\ { .0. } =/= Q ) ) |
13 |
9 11 12
|
sylanbrc |
|- ( ph -> { .0. } C. Q ) |
14 |
13 5
|
psssstrd |
|- ( ph -> { .0. } C. U ) |
15 |
14
|
pssned |
|- ( ph -> { .0. } =/= U ) |
16 |
15
|
necomd |
|- ( ph -> U =/= { .0. } ) |