Theorem lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lsatelb.v	|- V = ( Base ` W )
	lsatelb.o	|- .0. = ( 0g ` W )
	lsatelb.n	|- N = ( LSpan ` W )
	lsatelb.a	|- A = ( LSAtoms ` W )
	lsatelb.w	|- ( ph -> W e. LVec )
	lsatelb.x	|- ( ph -> X e. ( V \ { .0. } ) )
	lsatelb.u	|- ( ph -> U e. A )
Assertion	lsatelbN	|- ( ph -> ( X e. U <-> U = ( N ` { X } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsatelb.v	|- V = ( Base ` W )
2		lsatelb.o	|- .0. = ( 0g ` W )
3		lsatelb.n	|- N = ( LSpan ` W )
4		lsatelb.a	|- A = ( LSAtoms ` W )
5		lsatelb.w	|- ( ph -> W e. LVec )
6		lsatelb.x	|- ( ph -> X e. ( V \ { .0. } ) )
7		lsatelb.u	|- ( ph -> U e. A )
8	5	adantr	|- ( ( ph /\ X e. U ) -> W e. LVec )
9	7	adantr	|- ( ( ph /\ X e. U ) -> U e. A )
10		simpr	|- ( ( ph /\ X e. U ) -> X e. U )
11		eldifsn	|- ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
12	6 11	sylib	|- ( ph -> ( X e. V /\ X =/= .0. ) )
13	12	simprd	|- ( ph -> X =/= .0. )
14	13	adantr	|- ( ( ph /\ X e. U ) -> X =/= .0. )
15	2 3 4 8 9 10 14	lsatel	|- ( ( ph /\ X e. U ) -> U = ( N ` { X } ) )
16		eqimss2	|- ( U = ( N ` { X } ) -> ( N ` { X } ) C_ U )
17	16	adantl	|- ( ( ph /\ U = ( N ` { X } ) ) -> ( N ` { X } ) C_ U )
18		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
19		lveclmod	|- ( W e. LVec -> W e. LMod )
20	5 19	syl	|- ( ph -> W e. LMod )
21	18 4 20 7	lsatlssel	|- ( ph -> U e. ( LSubSp ` W ) )
22	6	eldifad	|- ( ph -> X e. V )
23	1 18 3 20 21 22	lspsnel5	|- ( ph -> ( X e. U <-> ( N ` { X } ) C_ U ) )
24	23	adantr	|- ( ( ph /\ U = ( N ` { X } ) ) -> ( X e. U <-> ( N ` { X } ) C_ U ) )
25	17 24	mpbird	|- ( ( ph /\ U = ( N ` { X } ) ) -> X e. U )
26	15 25	impbida	|- ( ph -> ( X e. U <-> U = ( N ` { X } ) ) )