# Metamath Proof Explorer

## Theorem lssatomic

Description: The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. ( shatomici analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lssatomic.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lssatomic.o
lssatomic.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
lssatomic.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lssatomic.u ${⊢}{\phi }\to {U}\in {S}$
lssatomic.n
Assertion lssatomic ${⊢}{\phi }\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\subseteq {U}$

### Proof

Step Hyp Ref Expression
1 lssatomic.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lssatomic.o
3 lssatomic.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
4 lssatomic.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 lssatomic.u ${⊢}{\phi }\to {U}\in {S}$
6 lssatomic.n
7 2 1 lssne0
8 5 7 syl
9 6 8 mpbid
12 simp2
13 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
14 13 1 lssel ${⊢}\left({U}\in {S}\wedge {x}\in {U}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
15 11 12 14 syl2anc
16 simp3
17 eqid ${⊢}\mathrm{LSpan}\left({W}\right)=\mathrm{LSpan}\left({W}\right)$
18 13 17 2 3 lsatlspsn2
19 10 15 16 18 syl3anc
20 1 17 10 11 12 lspsnel5a
21 sseq1 ${⊢}{q}=\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\to \left({q}\subseteq {U}↔\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\subseteq {U}\right)$
22 21 rspcev ${⊢}\left(\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\in {A}\wedge \mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\subseteq {U}\right)\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\subseteq {U}$
23 19 20 22 syl2anc
24 23 rexlimdv3a
25 9 24 mpd ${⊢}{\phi }\to \exists {q}\in {A}\phantom{\rule{.4em}{0ex}}{q}\subseteq {U}$