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 0˙=0W
lss0cl.s S=LSubSpW
Assertion lss0cl WLModUS0˙U

Proof

Step Hyp Ref Expression
1 lss0cl.z 0˙=0W
2 lss0cl.s S=LSubSpW
3 2 lssn0 USU
4 n0 UxxU
5 3 4 sylib USxxU
6 5 adantl WLModUSxxU
7 simp1 WLModUSxUWLMod
8 eqid BaseW=BaseW
9 8 2 lssel USxUxBaseW
10 9 3adant1 WLModUSxUxBaseW
11 eqid -W=-W
12 8 1 11 lmodsubid WLModxBaseWx-Wx=0˙
13 7 10 12 syl2anc WLModUSxUx-Wx=0˙
14 11 2 lssvsubcl WLModUSxUxUx-WxU
15 14 anabsan2 WLModUSxUx-WxU
16 15 3impa WLModUSxUx-WxU
17 13 16 eqeltrrd WLModUSxU0˙U
18 17 3expia WLModUSxU0˙U
19 18 exlimdv WLModUSxxU0˙U
20 6 19 mpd WLModUS0˙U