Metamath Proof Explorer

Theorem lss1

Description: The set of vectors in a left module is a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lssss.v ⊢V=BaseW
lssss.s ⊢S=LSubSp⁡W
Assertion lss1 ⊢W∈LMod→V∈S

Proof

Step Hyp Ref Expression
1 lssss.v ⊢V=BaseW
2 lssss.s ⊢S=LSubSp⁡W
3 eqidd ⊢W∈LMod→Scalar⁡W=Scalar⁡W
4 eqidd ⊢W∈LMod→BaseScalar⁡W=BaseScalar⁡W
5 1 a1i ⊢W∈LMod→V=BaseW
6 eqidd ⊢W∈LMod→+W=+W
7 eqidd ⊢W∈LMod→⋅W=⋅W
8 2 a1i ⊢W∈LMod→S=LSubSp⁡W
9 ssidd ⊢W∈LMod→V⊆V
10 1 lmodbn0 ⊢W∈LMod→V≠∅
11 simpl ⊢W∈LMod∧x∈BaseScalar⁡W∧a∈V∧b∈V→W∈LMod
12 eqid ⊢Scalar⁡W=Scalar⁡W
13 eqid ⊢⋅W=⋅W
14 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
15 1 12 13 14 lmodvscl ⊢W∈LMod∧x∈BaseScalar⁡W∧a∈V→x⋅Wa∈V
16 15 3adant3r3 ⊢W∈LMod∧x∈BaseScalar⁡W∧a∈V∧b∈V→x⋅Wa∈V
17 simpr3 ⊢W∈LMod∧x∈BaseScalar⁡W∧a∈V∧b∈V→b∈V
18 eqid ⊢+W=+W
19 1 18 lmodvacl ⊢W∈LMod∧x⋅Wa∈V∧b∈V→x⋅Wa+Wb∈V
20 11 16 17 19 syl3anc ⊢W∈LMod∧x∈BaseScalar⁡W∧a∈V∧b∈V→x⋅Wa+Wb∈V
21 3 4 5 6 7 8 9 10 20 islssd ⊢W∈LMod→V∈S