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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lsatlss.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
Assertion	lsatlss	⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lsatlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lsatlss.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
5		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6	3 4 5 2	lsatset	⊢ ( 𝑊 ∈ LMod → 𝐴 = ran ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ↦ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
7		eldifi	⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
8	3 1 4	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∈ 𝑆 )
9	7 8	sylan2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∈ 𝑆 )
10	9	fmpttd	⊢ ( 𝑊 ∈ LMod → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ↦ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) : ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⟶ 𝑆 )
11	10	frnd	⊢ ( 𝑊 ∈ LMod → ran ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ↦ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ⊆ 𝑆 )
12	6 11	eqsstrd	⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )