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

Metamath Proof Explorer

Theorem lshpne0

Description: The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014) (Proof shortened by AV, 19-Jul-2022)

		Ref	Expression
	Hypotheses	lshpne0.v	$⊢ V = {Base}_{W}$
		lshpne0.n	$⊢ N = LSpan (W)$
		lshpne0.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
		lshpne0.h	$⊢ H = LSHyp (W)$
		lshpne0.o	$⊢ \underset{˙}{0} = 0_{W}$
		lshpne0.w	$⊢ φ \to W \in LMod$
		lshpne0.u	$⊢ φ \to U \in H$
		lshpne0.x	$⊢ φ \to X \in V$
		lshpne0.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = V$
	Assertion	lshpne0	$⊢ φ \to X \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lshpne0.v	$⊢ V = {Base}_{W}$
2		lshpne0.n	$⊢ N = LSpan (W)$
3		lshpne0.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lshpne0.h	$⊢ H = LSHyp (W)$
5		lshpne0.o	$⊢ \underset{˙}{0} = 0_{W}$
6		lshpne0.w	$⊢ φ \to W \in LMod$
7		lshpne0.u	$⊢ φ \to U \in H$
8		lshpne0.x	$⊢ φ \to X \in V$
9		lshpne0.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = V$
10		eqid	$⊢ LSubSp (W) = LSubSp (W)$
11	10 4 6 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
12	1 2 3 4 6 7 8 9	lshpnel	$⊢ φ \to \neg X \in U$
13	5 10 6 11 12	lssvneln0	$⊢ φ \to X \neq \underset{˙}{0}$