Theorem islsati

Description: A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014)

	Ref	Expression
Hypotheses	islsati.v	|- V = ( Base ` W )
	islsati.n	|- N = ( LSpan ` W )
	islsati.a	|- A = ( LSAtoms ` W )
Assertion	islsati	|- ( ( W e. X /\ U e. A ) -> E. v e. V U = ( N ` { v } ) )

Proof

Step	Hyp	Ref	Expression
1		islsati.v	|- V = ( Base ` W )
2		islsati.n	|- N = ( LSpan ` W )
3		islsati.a	|- A = ( LSAtoms ` W )
4		difss	|- ( V \ { ( 0g ` W ) } ) C_ V
5		eqid	|- ( 0g ` W ) = ( 0g ` W )
6	1 2 5 3	islsat	|- ( W e. X -> ( U e. A <-> E. v e. ( V \ { ( 0g ` W ) } ) U = ( N ` { v } ) ) )
7	6	biimpa	|- ( ( W e. X /\ U e. A ) -> E. v e. ( V \ { ( 0g ` W ) } ) U = ( N ` { v } ) )
8		ssrexv	|- ( ( V \ { ( 0g ` W ) } ) C_ V -> ( E. v e. ( V \ { ( 0g ` W ) } ) U = ( N ` { v } ) -> E. v e. V U = ( N ` { v } ) ) )
9	4 7 8	mpsyl	|- ( ( W e. X /\ U e. A ) -> E. v e. V U = ( N ` { v } ) )