Theorem lsatel

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatel.o	|- .0. = ( 0g ` W )
	lsatel.n	|- N = ( LSpan ` W )
	lsatel.a	|- A = ( LSAtoms ` W )
	lsatel.w	|- ( ph -> W e. LVec )
	lsatel.u	|- ( ph -> U e. A )
	lsatel.x	|- ( ph -> X e. U )
	lsatel.e	|- ( ph -> X =/= .0. )
Assertion	lsatel	|- ( ph -> U = ( N ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatel.o	|- .0. = ( 0g ` W )
2		lsatel.n	|- N = ( LSpan ` W )
3		lsatel.a	|- A = ( LSAtoms ` W )
4		lsatel.w	|- ( ph -> W e. LVec )
5		lsatel.u	|- ( ph -> U e. A )
6		lsatel.x	|- ( ph -> X e. U )
7		lsatel.e	|- ( ph -> X =/= .0. )
8		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
9		lveclmod	|- ( W e. LVec -> W e. LMod )
10	4 9	syl	|- ( ph -> W e. LMod )
11	8 3 10 5	lsatlssel	|- ( ph -> U e. ( LSubSp ` W ) )
12	8 2 10 11 6	ellspsn5	|- ( ph -> ( N ` { X } ) C_ U )
13		eqid	|- ( Base ` W ) = ( Base ` W )
14	13 8	lssel	|- ( ( U e. ( LSubSp ` W ) /\ X e. U ) -> X e. ( Base ` W ) )
15	11 6 14	syl2anc	|- ( ph -> X e. ( Base ` W ) )
16	13 2 1 3	lsatlspsn2	|- ( ( W e. LMod /\ X e. ( Base ` W ) /\ X =/= .0. ) -> ( N ` { X } ) e. A )
17	10 15 7 16	syl3anc	|- ( ph -> ( N ` { X } ) e. A )
18	3 4 17 5	lsatcmp	|- ( ph -> ( ( N ` { X } ) C_ U <-> ( N ` { X } ) = U ) )
19	12 18	mpbid	|- ( ph -> ( N ` { X } ) = U )
20	19	eqcomd	|- ( ph -> U = ( N ` { X } ) )