# 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}={\mathrm{Base}}_{{W}}$
lssss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lss1 ${⊢}{W}\in \mathrm{LMod}\to {V}\in {S}$

### Proof

Step Hyp Ref Expression
1 lssss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lssss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 eqidd ${⊢}{W}\in \mathrm{LMod}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
4 eqidd ${⊢}{W}\in \mathrm{LMod}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
5 1 a1i ${⊢}{W}\in \mathrm{LMod}\to {V}={\mathrm{Base}}_{{W}}$
6 eqidd ${⊢}{W}\in \mathrm{LMod}\to {+}_{{W}}={+}_{{W}}$
7 eqidd ${⊢}{W}\in \mathrm{LMod}\to {\cdot }_{{W}}={\cdot }_{{W}}$
8 2 a1i ${⊢}{W}\in \mathrm{LMod}\to {S}=\mathrm{LSubSp}\left({W}\right)$
9 ssidd ${⊢}{W}\in \mathrm{LMod}\to {V}\subseteq {V}$
10 1 lmodbn0 ${⊢}{W}\in \mathrm{LMod}\to {V}\ne \varnothing$
11 simpl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to {W}\in \mathrm{LMod}$
12 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
13 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
14 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
15 1 12 13 14 lmodvscl ${⊢}\left({W}\in \mathrm{LMod}\wedge {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\right)\to {x}{\cdot }_{{W}}{a}\in {V}$
16 15 3adant3r3 ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to {x}{\cdot }_{{W}}{a}\in {V}$
17 simpr3 ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to {b}\in {V}$
18 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
19 1 18 lmodvacl ${⊢}\left({W}\in \mathrm{LMod}\wedge {x}{\cdot }_{{W}}{a}\in {V}\wedge {b}\in {V}\right)\to \left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}{b}\in {V}$
20 11 16 17 19 syl3anc ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to \left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}{b}\in {V}$
21 3 4 5 6 7 8 9 10 20 islssd ${⊢}{W}\in \mathrm{LMod}\to {V}\in {S}$