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