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{˙}{0} = 0_{W}$
	lsatnle.s	$⊢ S = LSubSp (W)$
	lsatnle.a	$⊢ A = LSAtoms (W)$
	lsatnle.w	$⊢ φ \to W \in LVec$
	lsatnle.u	$⊢ φ \to U \in S$
	lsatnle.q	$⊢ φ \to Q \in A$
Assertion	lsatnle	$⊢ φ \to (\neg Q \subseteq U \leftrightarrow U \cap Q = \{\underset{˙}{0}\})$

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

Metamath Proof Explorer