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

Metamath Proof Explorer

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. } ) )