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	$⊢ \underset{˙}{0} = 0_{W}$
	lssneln0.s	$⊢ S = LSubSp (W)$
	lssneln0.w	$⊢ φ \to W \in LMod$
	lssneln0.u	$⊢ φ \to U \in S$
	lssneln0.x	$⊢ φ \to X \in V$
	lssneln0.n	$⊢ φ \to \neg X \in U$
Assertion	lssneln0	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		lssneln0.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lssneln0.s	$⊢ S = LSubSp (W)$
3		lssneln0.w	$⊢ φ \to W \in LMod$
4		lssneln0.u	$⊢ φ \to U \in S$
5		lssneln0.x	$⊢ φ \to X \in V$
6		lssneln0.n	$⊢ φ \to \neg X \in U$
7	1 2 3 4 6	lssvneln0	$⊢ φ \to X \neq \underset{˙}{0}$
8		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
9	5 7 8	sylanbrc	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$