Metamath Proof Explorer


Theorem lsatssv

Description: An atom is a set of vectors. (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses lsatssv.v 𝑉 = ( Base ‘ 𝑊 )
lsatssv.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatssv.w ( 𝜑𝑊 ∈ LMod )
lsatssv.g ( 𝜑𝑄𝐴 )
Assertion lsatssv ( 𝜑𝑄𝑉 )

Proof

Step Hyp Ref Expression
1 lsatssv.v 𝑉 = ( Base ‘ 𝑊 )
2 lsatssv.a 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatssv.w ( 𝜑𝑊 ∈ LMod )
4 lsatssv.g ( 𝜑𝑄𝐴 )
5 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
6 5 2 3 4 lsatlssel ( 𝜑𝑄 ∈ ( LSubSp ‘ 𝑊 ) )
7 1 5 lssss ( 𝑄 ∈ ( LSubSp ‘ 𝑊 ) → 𝑄𝑉 )
8 6 7 syl ( 𝜑𝑄𝑉 )