This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )