Theorem 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={\mathrm{Base}}_W$$
	lshpdisj.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lshpdisj.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lshpdisj.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lshpdisj.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpdisj.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lshpdisj.u	$$⊢\phi \to U\in H$$
	lshpdisj.x	$$⊢\phi \to X\in V$$
	lshpdisj.e	$$⊢\phi \to U\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V$$
Assertion	lshpdisj	$$⊢\phi \to U\cap N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

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