Theorem lkrshp3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014)

	Ref	Expression
Hypotheses	lkrshp3.v	|- V = ( Base ` W )
	lkrshp3.d	|- D = ( Scalar ` W )
	lkrshp3.o	|- .0. = ( 0g ` D )
	lkrshp3.h	|- H = ( LSHyp ` W )
	lkrshp3.f	|- F = ( LFnl ` W )
	lkrshp3.k	|- K = ( LKer ` W )
	lkrshp3.w	|- ( ph -> W e. LVec )
	lkrshp3.g	|- ( ph -> G e. F )
Assertion	lkrshp3	|- ( ph -> ( ( K ` G ) e. H <-> G =/= ( V X. { .0. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshp3.v	|- V = ( Base ` W )
2		lkrshp3.d	|- D = ( Scalar ` W )
3		lkrshp3.o	|- .0. = ( 0g ` D )
4		lkrshp3.h	|- H = ( LSHyp ` W )
5		lkrshp3.f	|- F = ( LFnl ` W )
6		lkrshp3.k	|- K = ( LKer ` W )
7		lkrshp3.w	|- ( ph -> W e. LVec )
8		lkrshp3.g	|- ( ph -> G e. F )
9		lveclmod	|- ( W e. LVec -> W e. LMod )
10	7 9	syl	|- ( ph -> W e. LMod )
11	10	adantr	|- ( ( ph /\ ( K ` G ) e. H ) -> W e. LMod )
12		simpr	|- ( ( ph /\ ( K ` G ) e. H ) -> ( K ` G ) e. H )
13	1 4 11 12	lshpne	|- ( ( ph /\ ( K ` G ) e. H ) -> ( K ` G ) =/= V )
14	2 3 1 5 6	lkr0f	|- ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
15	10 8 14	syl2anc	|- ( ph -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
16	15	adantr	|- ( ( ph /\ ( K ` G ) e. H ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
17	16	necon3bid	|- ( ( ph /\ ( K ` G ) e. H ) -> ( ( K ` G ) =/= V <-> G =/= ( V X. { .0. } ) ) )
18	13 17	mpbid	|- ( ( ph /\ ( K ` G ) e. H ) -> G =/= ( V X. { .0. } ) )
19	7	adantr	|- ( ( ph /\ G =/= ( V X. { .0. } ) ) -> W e. LVec )
20	8	adantr	|- ( ( ph /\ G =/= ( V X. { .0. } ) ) -> G e. F )
21		simpr	|- ( ( ph /\ G =/= ( V X. { .0. } ) ) -> G =/= ( V X. { .0. } ) )
22	1 2 3 4 5 6	lkrshp	|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )
23	19 20 21 22	syl3anc	|- ( ( ph /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )
24	18 23	impbida	|- ( ph -> ( ( K ` G ) e. H <-> G =/= ( V X. { .0. } ) ) )