Theorem lduallkr3

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

	Ref	Expression
Hypotheses	lduallkr3.h	|- H = ( LSHyp ` W )
	lduallkr3.f	|- F = ( LFnl ` W )
	lduallkr3.k	|- K = ( LKer ` W )
	lduallkr3.d	|- D = ( LDual ` W )
	lduallkr3.o	|- .0. = ( 0g ` D )
	lduallkr3.w	|- ( ph -> W e. LVec )
	lduallkr3.g	|- ( ph -> G e. F )
Assertion	lduallkr3	|- ( ph -> ( ( K ` G ) e. H <-> G =/= .0. ) )

Proof

Step	Hyp	Ref	Expression
1		lduallkr3.h	|- H = ( LSHyp ` W )
2		lduallkr3.f	|- F = ( LFnl ` W )
3		lduallkr3.k	|- K = ( LKer ` W )
4		lduallkr3.d	|- D = ( LDual ` W )
5		lduallkr3.o	|- .0. = ( 0g ` D )
6		lduallkr3.w	|- ( ph -> W e. LVec )
7		lduallkr3.g	|- ( ph -> G e. F )
8		eqid	|- ( Base ` W ) = ( Base ` W )
9		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
10		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
11	8 9 10 1 2 3 6 7	lkrshp3	|- ( ph -> ( ( K ` G ) e. H <-> G =/= ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
12		lveclmod	|- ( W e. LVec -> W e. LMod )
13	6 12	syl	|- ( ph -> W e. LMod )
14	8 9 10 4 5 13	ldual0v	|- ( ph -> .0. = ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) )
15	14	neeq2d	|- ( ph -> ( G =/= .0. <-> G =/= ( ( Base ` W ) X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
16	11 15	bitr4d	|- ( ph -> ( ( K ` G ) e. H <-> G =/= .0. ) )