Theorem lduallkr3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015)

	Ref	Expression
Hypotheses	lduallkr3.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lduallkr3.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lduallkr3.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
	lduallkr3.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lduallkr3.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lduallkr3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lduallkr3.g	$$⊢\phi \to G\in F$$
Assertion	lduallkr3	$$⊢\phi \to \left(K\left(G\right)\in H\leftrightarrow G\ne \underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lduallkr3.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
2		lduallkr3.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
3		lduallkr3.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
4		lduallkr3.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		lduallkr3.o	$$⊢\underset{\dot{}}{0}=0_D$$
6		lduallkr3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lduallkr3.g	$$⊢\phi \to G\in F$$
8		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
9		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
10		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
11	8 9 10 1 2 3 6 7	lkrshp3	$$⊢\phi \to \left(K\left(G\right)\in H\leftrightarrow G\ne {\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
12		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
13	6 12	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
14	8 9 10 4 5 13	ldual0v	$$⊢\phi \to \underset{\dot{}}{0}={\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}$$
15	14	neeq2d	$$⊢\phi \to \left(G\ne \underset{\dot{}}{0}\leftrightarrow G\ne {\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
16	11 15	bitr4d	$$⊢\phi \to \left(K\left(G\right)\in H\leftrightarrow G\ne \underset{\dot{}}{0}\right)$$