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

Metamath Proof Explorer

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