Theorem lkrshp4

Description: A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014)

	Ref	Expression
Hypotheses	lkrshp4.v	$$⊢V={\mathrm{Base}}_W$$
	lkrshp4.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lkrshp4.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrshp4.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
	lkrshp4.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lkrshp4.g	$$⊢\phi \to G\in F$$
Assertion	lkrshp4	$$⊢\phi \to \left(K\left(G\right)\ne V\leftrightarrow K\left(G\right)\in H\right)$$

Proof

Step	Hyp	Ref	Expression
1		lkrshp4.v	$$⊢V={\mathrm{Base}}_W$$
2		lkrshp4.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
3		lkrshp4.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lkrshp4.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
5		lkrshp4.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lkrshp4.g	$$⊢\phi \to G\in F$$
7	1 2 3 4 5 6	lkrshpor	$$⊢\phi \to \left(K\left(G\right)\in H\vee K\left(G\right)=V\right)$$
8	7	orcomd	$$⊢\phi \to \left(K\left(G\right)=V\vee K\left(G\right)\in H\right)$$
9		neor	$$⊢\left(K\left(G\right)=V\vee K\left(G\right)\in H\right)\leftrightarrow \left(K\left(G\right)\ne V\to K\left(G\right)\in H\right)$$
10	8 9	sylib	$$⊢\phi \to \left(K\left(G\right)\ne V\to K\left(G\right)\in H\right)$$
11		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
12	5 11	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
13	12	adantr	$$⊢\left(\phi \wedge K\left(G\right)\in H\right)\to W\in \mathrm{LMod}$$
14		simpr	$$⊢\left(\phi \wedge K\left(G\right)\in H\right)\to K\left(G\right)\in H$$
15	1 2 13 14	lshpne	$$⊢\left(\phi \wedge K\left(G\right)\in H\right)\to K\left(G\right)\ne V$$
16	15	ex	$$⊢\phi \to \left(K\left(G\right)\in H\to K\left(G\right)\ne V\right)$$
17	10 16	impbid	$$⊢\phi \to \left(K\left(G\right)\ne V\leftrightarrow K\left(G\right)\in H\right)$$