lshpnel

Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lshpnel.v	$⊢ V = {Base}_{W}$
2		lshpnel.n	$⊢ N = LSpan (W)$
3		lshpnel.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		lshpnel.h	$⊢ H = LSHyp (W)$
5		lshpnel.w	$⊢ φ \to W \in LMod$
6		lshpnel.u	$⊢ φ \to U \in H$
7		lshpnel.x	$⊢ φ \to X \in V$
8		lshpnel.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = V$
9	1 4 5 6	lshpne	$⊢ φ \to U \neq V$
10	5	adantr	$⊢ (φ \land X \in U) \to W \in LMod$
11		eqid	$⊢ LSubSp (W) = LSubSp (W)$
12	11	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
13	10 12	syl	$⊢ (φ \land X \in U) \to LSubSp (W) \subseteq SubGrp (W)$
14	11 4 5 6	lshplss	$⊢ φ \to U \in LSubSp (W)$
15	14	adantr	$⊢ (φ \land X \in U) \to U \in LSubSp (W)$
16	13 15	sseldd	$⊢ (φ \land X \in U) \to U \in SubGrp (W)$
17	7	adantr	$⊢ (φ \land X \in U) \to X \in V$
18	1 11 2	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
19	10 17 18	syl2anc	$⊢ (φ \land X \in U) \to N (\{X\}) \in LSubSp (W)$
20	13 19	sseldd	$⊢ (φ \land X \in U) \to N (\{X\}) \in SubGrp (W)$
21		simpr	$⊢ (φ \land X \in U) \to X \in U$
22	11 2 10 15 21	lspsnel5a	$⊢ (φ \land X \in U) \to N (\{X\}) \subseteq U$
23	3	lsmss2	$⊢ (U \in SubGrp (W) \land N (\{X\}) \in SubGrp (W) \land N (\{X\}) \subseteq U) \to U \underset{˙}{\oplus} N (\{X\}) = U$
24	16 20 22 23	syl3anc	$⊢ (φ \land X \in U) \to U \underset{˙}{\oplus} N (\{X\}) = U$
25	8	adantr	$⊢ (φ \land X \in U) \to U \underset{˙}{\oplus} N (\{X\}) = V$
26	24 25	eqtr3d	$⊢ (φ \land X \in U) \to U = V$
27	26	ex	$⊢ φ \to (X \in U \to U = V)$
28	27	necon3ad	$⊢ φ \to (U \neq V \to \neg X \in U)$
29	9 28	mpd	$⊢ φ \to \neg X \in U$

Metamath Proof Explorer

Theorem lshpnel

Proof