Theorem lssneln0

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

	Ref	Expression
Hypotheses	lssneln0.o	|- .0. = ( 0g ` W )
	lssneln0.s	|- S = ( LSubSp ` W )
	lssneln0.w	|- ( ph -> W e. LMod )
	lssneln0.u	|- ( ph -> U e. S )
	lssneln0.x	|- ( ph -> X e. V )
	lssneln0.n	|- ( ph -> -. X e. U )
Assertion	lssneln0	|- ( ph -> X e. ( V \ { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lssneln0.o	|- .0. = ( 0g ` W )
2		lssneln0.s	|- S = ( LSubSp ` W )
3		lssneln0.w	|- ( ph -> W e. LMod )
4		lssneln0.u	|- ( ph -> U e. S )
5		lssneln0.x	|- ( ph -> X e. V )
6		lssneln0.n	|- ( ph -> -. X e. U )
7	1 2 3 4 6	lssvneln0	|- ( ph -> X =/= .0. )
8		eldifsn	|- ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
9	5 7 8	sylanbrc	|- ( ph -> X e. ( V \ { .0. } ) )