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	$$⊢\underset{\dot{}}{0}=0_W$$
	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	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$
Assertion	lssatomic	$$⊢\phi \to \exists q\in Aq\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		lssatomic.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lssatomic.o	$$⊢\underset{\dot{}}{0}=0_W$$
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	$$⊢\phi \to U\ne \left\{\underset{\dot{}}{0}\right\}$$
7	2 1	lssne0	$$⊢U\in S\to \left(U\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \exists x\in Ux\ne \underset{\dot{}}{0}\right)$$
8	5 7	syl	$$⊢\phi \to \left(U\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \exists x\in Ux\ne \underset{\dot{}}{0}\right)$$
9	6 8	mpbid	$$⊢\phi \to \exists x\in Ux\ne \underset{\dot{}}{0}$$
10	4	3ad2ant1	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to W\in \mathrm{LMod}$$
11	5	3ad2ant1	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to U\in S$$
12		simp2	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to x\in U$$
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	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to x\in {\mathrm{Base}}_W$$
16		simp3	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to x\ne \underset{\dot{}}{0}$$
17		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
18	13 17 2 3	lsatlspsn2	$$⊢\left(W\in \mathrm{LMod}\wedge x\in {\mathrm{Base}}_W\wedge x\ne \underset{\dot{}}{0}\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{x\right\}\right)\in A$$
19	10 15 16 18	syl3anc	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{x\right\}\right)\in A$$
20	1 17 10 11 12	lspsnel5a	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{x\right\}\right)\subseteq U$$
21		sseq1	$$⊢q=\mathrm{LSpan}\left(W\right)\left(\left\{x\right\}\right)\to \left(q\subseteq U\leftrightarrow \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 Aq\subseteq U$$
23	19 20 22	syl2anc	$$⊢\left(\phi \wedge x\in U\wedge x\ne \underset{\dot{}}{0}\right)\to \exists q\in Aq\subseteq U$$
24	23	rexlimdv3a	$$⊢\phi \to \left(\exists x\in Ux\ne \underset{\dot{}}{0}\to \exists q\in Aq\subseteq U\right)$$
25	9 24	mpd	$$⊢\phi \to \exists q\in Aq\subseteq U$$