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 )