Theorem lssvneln0

Description: A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015) (Revised by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lssvneln0.o	|- .0. = ( 0g ` W )
	lssvneln0.s	|- S = ( LSubSp ` W )
	lssvneln0.w	|- ( ph -> W e. LMod )
	lssvneln0.u	|- ( ph -> U e. S )
	lssvneln0.n	|- ( ph -> -. X e. U )
Assertion	lssvneln0	|- ( ph -> X =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		lssvneln0.o	|- .0. = ( 0g ` W )
2		lssvneln0.s	|- S = ( LSubSp ` W )
3		lssvneln0.w	|- ( ph -> W e. LMod )
4		lssvneln0.u	|- ( ph -> U e. S )
5		lssvneln0.n	|- ( ph -> -. X e. U )
6	1 2	lss0cl	|- ( ( W e. LMod /\ U e. S ) -> .0. e. U )
7	3 4 6	syl2anc	|- ( ph -> .0. e. U )
8		eleq1a	|- ( .0. e. U -> ( X = .0. -> X e. U ) )
9	7 8	syl	|- ( ph -> ( X = .0. -> X e. U ) )
10	9	necon3bd	|- ( ph -> ( -. X e. U -> X =/= .0. ) )
11	5 10	mpd	|- ( ph -> X =/= .0. )