This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. = ( 0g ` W )
lss0cl.s 
|- S = ( LSubSp ` W )
Assertion lss0cl 
|- ( ( W e. LMod /\ U e. S ) -> .0. e. U )

Proof

Step Hyp Ref Expression
1 lss0cl.z 
 |-  .0. = ( 0g ` W )
2 lss0cl.s 
 |-  S = ( LSubSp ` W )
3 2 lssn0 
 |-  ( U e. S -> U =/= (/) )
4 n0 
 |-  ( U =/= (/) <-> E. x x e. U )
5 3 4 sylib 
 |-  ( U e. S -> E. x x e. U )
6 5 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> E. x x e. U )
7 simp1 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> W e. LMod )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 8 2 lssel 
 |-  ( ( U e. S /\ x e. U ) -> x e. ( Base ` W ) )
10 9 3adant1 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> x e. ( Base ` W ) )
11 eqid 
 |-  ( -g ` W ) = ( -g ` W )
12 8 1 11 lmodsubid 
 |-  ( ( W e. LMod /\ x e. ( Base ` W ) ) -> ( x ( -g ` W ) x ) = .0. )
13 7 10 12 syl2anc 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> ( x ( -g ` W ) x ) = .0. )
14 11 2 lssvsubcl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. U /\ x e. U ) ) -> ( x ( -g ` W ) x ) e. U )
15 14 anabsan2 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> ( x ( -g ` W ) x ) e. U )
16 15 3impa 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> ( x ( -g ` W ) x ) e. U )
17 13 16 eqeltrrd 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> .0. e. U )
18 17 3expia 
 |-  ( ( W e. LMod /\ U e. S ) -> ( x e. U -> .0. e. U ) )
19 18 exlimdv 
 |-  ( ( W e. LMod /\ U e. S ) -> ( E. x x e. U -> .0. e. U ) )
20 6 19 mpd 
 |-  ( ( W e. LMod /\ U e. S ) -> .0. e. U )