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 = ( Base ` W )
	lkrshp4.h	|- H = ( LSHyp ` W )
	lkrshp4.f	|- F = ( LFnl ` W )
	lkrshp4.k	|- K = ( LKer ` W )
	lkrshp4.w	|- ( ph -> W e. LVec )
	lkrshp4.g	|- ( ph -> G e. F )
Assertion	lkrshp4	|- ( ph -> ( ( K ` G ) =/= V <-> ( K ` G ) e. H ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshp4.v	|- V = ( Base ` W )
2		lkrshp4.h	|- H = ( LSHyp ` W )
3		lkrshp4.f	|- F = ( LFnl ` W )
4		lkrshp4.k	|- K = ( LKer ` W )
5		lkrshp4.w	|- ( ph -> W e. LVec )
6		lkrshp4.g	|- ( ph -> G e. F )
7	1 2 3 4 5 6	lkrshpor	|- ( ph -> ( ( K ` G ) e. H \/ ( K ` G ) = V ) )
8	7	orcomd	|- ( ph -> ( ( K ` G ) = V \/ ( K ` G ) e. H ) )
9		neor	|- ( ( ( K ` G ) = V \/ ( K ` G ) e. H ) <-> ( ( K ` G ) =/= V -> ( K ` G ) e. H ) )
10	8 9	sylib	|- ( ph -> ( ( K ` G ) =/= V -> ( K ` G ) e. H ) )
11		lveclmod	|- ( W e. LVec -> W e. LMod )
12	5 11	syl	|- ( ph -> W e. LMod )
13	12	adantr	|- ( ( ph /\ ( K ` G ) e. H ) -> W e. LMod )
14		simpr	|- ( ( ph /\ ( K ` G ) e. H ) -> ( K ` G ) e. H )
15	1 2 13 14	lshpne	|- ( ( ph /\ ( K ` G ) e. H ) -> ( K ` G ) =/= V )
16	15	ex	|- ( ph -> ( ( K ` G ) e. H -> ( K ` G ) =/= V ) )
17	10 16	impbid	|- ( ph -> ( ( K ` G ) =/= V <-> ( K ` G ) e. H ) )