This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )