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

Metamath Proof Explorer

Theorem lsatlss

Description: The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lsatlss.s 
|- S = ( LSubSp ` W )
lsatlss.a 
|- A = ( LSAtoms ` W )
Assertion lsatlss 
|- ( W e. LMod -> A C_ S )

Proof

Step Hyp Ref Expression
1 lsatlss.s 
 |-  S = ( LSubSp ` W )
2 lsatlss.a 
 |-  A = ( LSAtoms ` W )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
5 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
6 3 4 5 2 lsatset 
 |-  ( W e. LMod -> A = ran ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) |-> ( ( LSpan ` W ) ` { v } ) ) )
7 eldifi 
 |-  ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) -> v e. ( Base ` W ) )
8 3 1 4 lspsncl 
 |-  ( ( W e. LMod /\ v e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { v } ) e. S )
9 7 8 sylan2 
 |-  ( ( W e. LMod /\ v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) ) -> ( ( LSpan ` W ) ` { v } ) e. S )
10 9 fmpttd 
 |-  ( W e. LMod -> ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) |-> ( ( LSpan ` W ) ` { v } ) ) : ( ( Base ` W ) \ { ( 0g ` W ) } ) --> S )
11 10 frnd 
 |-  ( W e. LMod -> ran ( v e. ( ( Base ` W ) \ { ( 0g ` W ) } ) |-> ( ( LSpan ` W ) ` { v } ) ) C_ S )
12 6 11 eqsstrd 
 |-  ( W e. LMod -> A C_ S )