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

Metamath Proof Explorer

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