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	|- .0. = ( 0g ` W )
	lsatnle.s	|- S = ( LSubSp ` W )
	lsatnle.a	|- A = ( LSAtoms ` W )
	lsatnle.w	|- ( ph -> W e. LVec )
	lsatnle.u	|- ( ph -> U e. S )
	lsatnle.q	|- ( ph -> Q e. A )
Assertion	lsatnle	|- ( ph -> ( -. Q C_ U <-> ( U i^i Q ) = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatnle.o	|- .0. = ( 0g ` W )
2		lsatnle.s	|- S = ( LSubSp ` W )
3		lsatnle.a	|- A = ( LSAtoms ` W )
4		lsatnle.w	|- ( ph -> W e. LVec )
5		lsatnle.u	|- ( ph -> U e. S )
6		lsatnle.q	|- ( ph -> Q e. A )
7		eqid	|- ( LSSum ` W ) = ( LSSum ` W )
8		eqid	|- (
9	2 7 3 8 4 5 6	lcv1	|- ( ph -> ( -. Q C_ U <-> U (
10	2 7 1 3 8 4 5 6	lcvp	|- ( ph -> ( ( U i^i Q ) = { .0. } <-> U (
11	9 10	bitr4d	|- ( ph -> ( -. Q C_ U <-> ( U i^i Q ) = { .0. } ) )