Theorem lsatnle

Description: The meet of a subspace and an incomparable atom is the zero subspace. ( atnssm0 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatnle.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsatnle.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lsatnle.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lsatnle.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lsatnle.u	$$⊢\phi \to U\in S$$
	lsatnle.q	$$⊢\phi \to Q\in A$$
Assertion	lsatnle	$$⊢\phi \to \left(\neg Q\subseteq U\leftrightarrow U\cap Q=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsatnle.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lsatnle.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lsatnle.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
4		lsatnle.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lsatnle.u	$$⊢\phi \to U\in S$$
6		lsatnle.q	$$⊢\phi \to Q\in A$$
7		eqid	$$⊢\mathrm{LSSum}\left(W\right)=\mathrm{LSSum}\left(W\right)$$
8		eqid	$$⊢{⋖}_L\left(W\right)={⋖}_L\left(W\right)$$
9	2 7 3 8 4 5 6	lcv1	$$⊢\phi \to \left(\neg Q\subseteq U\leftrightarrow U{⋖}_L\left(W\right)\left(U\mathrm{LSSum}\left(W\right)Q\right)\right)$$
10	2 7 1 3 8 4 5 6	lcvp	$$⊢\phi \to \left(U\cap Q=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow U{⋖}_L\left(W\right)\left(U\mathrm{LSSum}\left(W\right)Q\right)\right)$$
11	9 10	bitr4d	$$⊢\phi \to \left(\neg Q\subseteq U\leftrightarrow U\cap Q=\left\{\underset{\dot{}}{0}\right\}\right)$$