# Metamath Proof Explorer

## Theorem lsssn0

Description: The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lss0cl.z
lss0cl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lsssn0

### Proof

Step Hyp Ref Expression
1 lss0cl.z
2 lss0cl.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 eqidd ${⊢}{W}\in \mathrm{LMod}\to {\mathrm{Base}}_{{W}}={\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 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
10 9 1 lmod0vcl
11 10 snssd
12 1 fvexi
13 12 snnz
14 13 a1i
15 simpr2
16 elsni
17 15 16 syl
18 17 oveq2d
19 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
20 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
21 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
22 19 20 21 1 lmodvs0
24 18 23 eqtrd
25 simpr3
26 elsni
27 25 26 syl
28 24 27 oveq12d
29 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
30 9 29 1 lmod0vlid
31 10 30 mpdan
34 ovex ${⊢}\left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}{b}\in \mathrm{V}$