Theorem lsatlspsn2

Description: The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn instead? (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lsatset.v	|- V = ( Base ` W )
	lsatset.n	|- N = ( LSpan ` W )
	lsatset.z	|- .0. = ( 0g ` W )
	lsatset.a	|- A = ( LSAtoms ` W )
Assertion	lsatlspsn2	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )

Proof

Step	Hyp	Ref	Expression
1		lsatset.v	|- V = ( Base ` W )
2		lsatset.n	|- N = ( LSpan ` W )
3		lsatset.z	|- .0. = ( 0g ` W )
4		lsatset.a	|- A = ( LSAtoms ` W )
5		3simpc	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( X e. V /\ X =/= .0. ) )
6		eldifsn	|- ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
7	5 6	sylibr	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> X e. ( V \ { .0. } ) )
8		eqid	|- ( N ` { X } ) = ( N ` { X } )
9		sneq	|- ( v = X -> { v } = { X } )
10	9	fveq2d	|- ( v = X -> ( N ` { v } ) = ( N ` { X } ) )
11	10	rspceeqv	|- ( ( X e. ( V \ { .0. } ) /\ ( N ` { X } ) = ( N ` { X } ) ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
12	7 8 11	sylancl	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) )
13	1 2 3 4	islsat	|- ( W e. LMod -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
14	13	3ad2ant1	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) )
15	12 14	mpbird	|- ( ( W e. LMod /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. A )