This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsatssv

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

Ref Expression
Hypotheses lsatssv.v ⊢ V = Base W
lsatssv.a ⊢ A = LSAtoms ⁡ W
lsatssv.w ⊢ φ → W ∈ LMod
lsatssv.g ⊢ φ → Q ∈ A
Assertion lsatssv ⊢ φ → Q ⊆ V

Proof

Step Hyp Ref Expression
1 lsatssv.v ⊢ V = Base W
2 lsatssv.a ⊢ A = LSAtoms ⁡ W
3 lsatssv.w ⊢ φ → W ∈ LMod
4 lsatssv.g ⊢ φ → Q ∈ A
5 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
6 5 2 3 4 lsatlssel ⊢ φ → Q ∈ LSubSp ⁡ W
7 1 5 lssss ⊢ Q ∈ LSubSp ⁡ W → Q ⊆ V
8 6 7 syl ⊢ φ → Q ⊆ V