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 )