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

Metamath Proof Explorer

Theorem lssss

Description: A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lssss.v ⊢ V = Base W
lssss.s ⊢ S = LSubSp ⁡ W
Assertion lssss ⊢ U ∈ S → U ⊆ V

Proof

Step Hyp Ref Expression
1 lssss.v ⊢ V = Base W
2 lssss.s ⊢ S = LSubSp ⁡ W
3 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
4 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
5 eqid ⊢ + W = + W
6 eqid ⊢ ⋅ W = ⋅ W
7 3 4 1 5 6 2 islss ⊢ U ∈ S ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ Base Scalar ⁡ W ∀ a ∈ U ∀ b ∈ U x ⋅ W a + W b ∈ U
8 7 simp1bi ⊢ U ∈ S → U ⊆ V