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 | ⊢ ( 𝜑 → 𝑄 ⊆ 𝑉 ) |
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 | ⊢ ( 𝜑 → 𝑄 ⊆ 𝑉 ) |