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 ⊢ 𝑆 = ( 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 → 𝐴 ⊆ 𝑆 )