Theorem lkrshpor

Description: The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014)

	Ref	Expression
Hypotheses	lkrshpor.v	|- V = ( Base ` W )
	lkrshpor.h	|- H = ( LSHyp ` W )
	lkrshpor.f	|- F = ( LFnl ` W )
	lkrshpor.k	|- K = ( LKer ` W )
	lkrshpor.w	|- ( ph -> W e. LVec )
	lkrshpor.g	|- ( ph -> G e. F )
Assertion	lkrshpor	|- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshpor.v	|- V = ( Base ` W )
2		lkrshpor.h	|- H = ( LSHyp ` W )
3		lkrshpor.f	|- F = ( LFnl ` W )
4		lkrshpor.k	|- K = ( LKer ` W )
5		lkrshpor.w	|- ( ph -> W e. LVec )
6		lkrshpor.g	|- ( ph -> G e. F )
7		lveclmod	|- ( W e. LVec -> W e. LMod )
8	5 7	syl	|- ( ph -> W e. LMod )
9		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
10		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
11	9 10 1 3 4	lkr0f	|- ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
12	8 6 11	syl2anc	|- ( ph -> ( ( K ` G ) = V <-> G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
13	12	biimpar	|- ( ( ph /\ G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( K ` G ) = V )
14	13	olcd	|- ( ( ph /\ G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
15	5	adantr	|- ( ( ph /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> W e. LVec )
16	6	adantr	|- ( ( ph /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> G e. F )
17		simpr	|- ( ( ph /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
18	1 9 10 2 3 4	lkrshp	|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( K ` G ) e. H )
19	15 16 17 18	syl3anc	|- ( ( ph /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( K ` G ) e. H )
20	19	orcd	|- ( ( ph /\ G =/= ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
21	14 20	pm2.61dane	|- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )