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)

Step	Hyp	Ref	Expression
1		lssvneln0.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lssvneln0.s	$⊢ S = LSubSp (W)$
3		lssvneln0.w	$⊢ φ \to W \in LMod$
4		lssvneln0.u	$⊢ φ \to U \in S$
5		lssvneln0.n	$⊢ φ \to \neg X \in U$
6	1 2	lss0cl	$⊢ (W \in LMod \land U \in S) \to \underset{˙}{0} \in U$
7	3 4 6	syl2anc	$⊢ φ \to \underset{˙}{0} \in U$
8		eleq1a	$⊢ \underset{˙}{0} \in U \to (X = \underset{˙}{0} \to X \in U)$
9	7 8	syl	$⊢ φ \to (X = \underset{˙}{0} \to X \in U)$
10	9	necon3bd	$⊢ φ \to (\neg X \in U \to X \neq \underset{˙}{0})$
11	5 10	mpd	$⊢ φ \to X \neq \underset{˙}{0}$

Metamath Proof Explorer