# Metamath Proof Explorer

## Theorem lss0cl

Description: The zero vector belongs to every subspace. (Contributed by NM, 12-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

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

### Proof

Step Hyp Ref Expression
1 lss0cl.z
2 lss0cl.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 2 lssn0 ${⊢}{U}\in {S}\to {U}\ne \varnothing$
4 n0 ${⊢}{U}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {U}$
5 3 4 sylib ${⊢}{U}\in {S}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {U}$
6 5 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {U}$
7 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\wedge {x}\in {U}\right)\to {W}\in \mathrm{LMod}$
8 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
9 8 2 lssel ${⊢}\left({U}\in {S}\wedge {x}\in {U}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
10 9 3adant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\wedge {x}\in {U}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
11 eqid ${⊢}{-}_{{W}}={-}_{{W}}$
12 8 1 11 lmodsubid
13 7 10 12 syl2anc
14 11 2 lssvsubcl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {U}\wedge {x}\in {U}\right)\right)\to {x}{-}_{{W}}{x}\in {U}$
15 14 anabsan2 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to {x}{-}_{{W}}{x}\in {U}$
16 15 3impa ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\wedge {x}\in {U}\right)\to {x}{-}_{{W}}{x}\in {U}$
17 13 16 eqeltrrd
18 17 3expia
19 18 exlimdv
20 6 19 mpd