lshpdisj

Description: A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lshpdisj.v	$⊢ V = {Base}_{W}$
2		lshpdisj.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lshpdisj.n	$⊢ N = LSpan (W)$
4		lshpdisj.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpdisj.h	$⊢ H = LSHyp (W)$
6		lshpdisj.w	$⊢ φ \to W \in LVec$
7		lshpdisj.u	$⊢ φ \to U \in H$
8		lshpdisj.x	$⊢ φ \to X \in V$
9		lshpdisj.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{X\}) = V$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	6 10	syl	$⊢ φ \to W \in LMod$
12	11	adantr	$⊢ (φ \land v \in U) \to W \in LMod$
13	8	adantr	$⊢ (φ \land v \in U) \to X \in V$
14		eqid	$⊢ Scalar (W) = Scalar (W)$
15		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
16		eqid	$⊢ \cdot_{W} = \cdot_{W}$
17	14 15 1 16 3	lspsnel	$⊢ (W \in LMod \land X \in V) \to (v \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X)$
18	12 13 17	syl2anc	$⊢ (φ \land v \in U) \to (v \in N (\{X\}) \leftrightarrow \exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X)$
19	1 3 4 5 11 7 8 9	lshpnel	$⊢ φ \to \neg X \in U$
20	19	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to \neg X \in U$
21		eqid	$⊢ LSubSp (W) = LSubSp (W)$
22	6	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to W \in LVec$
23	21 5 11 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
24	23	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to U \in LSubSp (W)$
25	8	ad2antrr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to X \in V$
26	11	adantr	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to W \in LMod$
27		simpr	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to k \in {Base}_{Scalar (W)}$
28	8	adantr	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to X \in V$
29	1 16 14 15 3 26 27 28	lspsneli	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to k \cdot_{W} X \in N (\{X\})$
30	29	adantr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to k \cdot_{W} X \in N (\{X\})$
31		simpr	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to k \cdot_{W} X \neq \underset{˙}{0}$
32	1 2 21 3 22 24 25 30 31	lspsnel4	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to (X \in U \leftrightarrow k \cdot_{W} X \in U)$
33	20 32	mtbid	$⊢ ((φ \land k \in {Base}_{Scalar (W)}) \land k \cdot_{W} X \neq \underset{˙}{0}) \to \neg k \cdot_{W} X \in U$
34	33	ex	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to (k \cdot_{W} X \neq \underset{˙}{0} \to \neg k \cdot_{W} X \in U)$
35	34	necon4ad	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to (k \cdot_{W} X \in U \to k \cdot_{W} X = \underset{˙}{0})$
36		eleq1	$⊢ v = k \cdot_{W} X \to (v \in U \leftrightarrow k \cdot_{W} X \in U)$
37		eqeq1	$⊢ v = k \cdot_{W} X \to (v = \underset{˙}{0} \leftrightarrow k \cdot_{W} X = \underset{˙}{0})$
38	36 37	imbi12d	$⊢ v = k \cdot_{W} X \to ((v \in U \to v = \underset{˙}{0}) \leftrightarrow (k \cdot_{W} X \in U \to k \cdot_{W} X = \underset{˙}{0}))$
39	35 38	syl5ibrcom	$⊢ (φ \land k \in {Base}_{Scalar (W)}) \to (v = k \cdot_{W} X \to (v \in U \to v = \underset{˙}{0}))$
40	39	ex	$⊢ φ \to (k \in {Base}_{Scalar (W)} \to (v = k \cdot_{W} X \to (v \in U \to v = \underset{˙}{0})))$
41	40	com23	$⊢ φ \to (v = k \cdot_{W} X \to (k \in {Base}_{Scalar (W)} \to (v \in U \to v = \underset{˙}{0})))$
42	41	com24	$⊢ φ \to (v \in U \to (k \in {Base}_{Scalar (W)} \to (v = k \cdot_{W} X \to v = \underset{˙}{0})))$
43	42	imp31	$⊢ ((φ \land v \in U) \land k \in {Base}_{Scalar (W)}) \to (v = k \cdot_{W} X \to v = \underset{˙}{0})$
44	43	rexlimdva	$⊢ (φ \land v \in U) \to (\exists k \in {Base}_{Scalar (W)} v = k \cdot_{W} X \to v = \underset{˙}{0})$
45	18 44	sylbid	$⊢ (φ \land v \in U) \to (v \in N (\{X\}) \to v = \underset{˙}{0})$
46	45	expimpd	$⊢ φ \to ((v \in U \land v \in N (\{X\})) \to v = \underset{˙}{0})$
47		elin	$⊢ v \in (U \cap N (\{X\})) \leftrightarrow (v \in U \land v \in N (\{X\}))$
48		velsn	$⊢ v \in \{\underset{˙}{0}\} \leftrightarrow v = \underset{˙}{0}$
49	46 47 48	3imtr4g	$⊢ φ \to (v \in (U \cap N (\{X\})) \to v \in \{\underset{˙}{0}\})$
50	49	ssrdv	$⊢ φ \to U \cap N (\{X\}) \subseteq \{\underset{˙}{0}\}$
51	1 21 3	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
52	11 8 51	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (W)$
53	21	lssincl	$⊢ (W \in LMod \land U \in LSubSp (W) \land N (\{X\}) \in LSubSp (W)) \to U \cap N (\{X\}) \in LSubSp (W)$
54	11 23 52 53	syl3anc	$⊢ φ \to U \cap N (\{X\}) \in LSubSp (W)$
55	2 21	lss0ss	$⊢ (W \in LMod \land U \cap N (\{X\}) \in LSubSp (W)) \to \{\underset{˙}{0}\} \subseteq U \cap N (\{X\})$
56	11 54 55	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} \subseteq U \cap N (\{X\})$
57	50 56	eqssd	$⊢ φ \to U \cap N (\{X\}) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lshpdisj

Proof