Theorem lsatnem0

Description: The meet of distinct atoms is the zero subspace. ( atnemeq0 analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lsatnem0.o	|- .0. = ( 0g ` W )
	lsatnem0.a	|- A = ( LSAtoms ` W )
	lsatnem0.w	|- ( ph -> W e. LVec )
	lsatnem0.q	|- ( ph -> Q e. A )
	lsatnem0.r	|- ( ph -> R e. A )
Assertion	lsatnem0	|- ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatnem0.o	|- .0. = ( 0g ` W )
2		lsatnem0.a	|- A = ( LSAtoms ` W )
3		lsatnem0.w	|- ( ph -> W e. LVec )
4		lsatnem0.q	|- ( ph -> Q e. A )
5		lsatnem0.r	|- ( ph -> R e. A )
6	2 3 5 4	lsatcmp	|- ( ph -> ( R C_ Q <-> R = Q ) )
7		eqcom	|- ( R = Q <-> Q = R )
8	6 7	bitrdi	|- ( ph -> ( R C_ Q <-> Q = R ) )
9	8	necon3bbid	|- ( ph -> ( -. R C_ Q <-> Q =/= R ) )
10		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
11		lveclmod	|- ( W e. LVec -> W e. LMod )
12	3 11	syl	|- ( ph -> W e. LMod )
13	10 2 12 4	lsatlssel	|- ( ph -> Q e. ( LSubSp ` W ) )
14	1 10 2 3 13 5	lsatnle	|- ( ph -> ( -. R C_ Q <-> ( Q i^i R ) = { .0. } ) )
15	9 14	bitr3d	|- ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )