Metamath Proof Explorer

Theorem lkrshp

Description: The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014)

Ref Expression
Hypotheses lkrshp.v 
|- V = ( Base ` W )
lkrshp.d 
|- D = ( Scalar ` W )
lkrshp.z 
|- .0. = ( 0g ` D )
lkrshp.h 
|- H = ( LSHyp ` W )
lkrshp.f 
|- F = ( LFnl ` W )
lkrshp.k 
|- K = ( LKer ` W )
Assertion lkrshp 
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )

Proof

Step Hyp Ref Expression
1 lkrshp.v 
 |-  V = ( Base ` W )
2 lkrshp.d 
 |-  D = ( Scalar ` W )
3 lkrshp.z 
 |-  .0. = ( 0g ` D )
4 lkrshp.h 
 |-  H = ( LSHyp ` W )
5 lkrshp.f 
 |-  F = ( LFnl ` W )
6 lkrshp.k 
 |-  K = ( LKer ` W )
7 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
8 7 3ad2ant1 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> W e. LMod )
9 simp2 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> G e. F )
10 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
11 5 6 10 lkrlss 
 |-  ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. ( LSubSp ` W ) )
12 8 9 11 syl2anc 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. ( LSubSp ` W ) )
13 simp3 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> G =/= ( V X. { .0. } ) )
14 2 3 1 5 6 lkr0f 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
15 8 9 14 syl2anc 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( ( K ` G ) = V <-> G = ( V X. { .0. } ) ) )
16 15 necon3bid 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( ( K ` G ) =/= V <-> G =/= ( V X. { .0. } ) ) )
17 13 16 mpbird 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) =/= V )
18 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
19 2 3 18 1 5 lfl1 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. v e. V ( G ` v ) = ( 1r ` D ) )
20 simp11 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> W e. LVec )
21 simp2 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> v e. V )
22 simp12 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> G e. F )
23 simp3 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( G ` v ) = ( 1r ` D ) )
24 2 lvecdrng 
 |-  ( W e. LVec -> D e. DivRing )
25 3 18 drngunz 
 |-  ( D e. DivRing -> ( 1r ` D ) =/= .0. )
26 20 24 25 3syl 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( 1r ` D ) =/= .0. )
27 23 26 eqnetrd 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( G ` v ) =/= .0. )
28 simpl11 
 |-  ( ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) /\ v e. ( K ` G ) ) -> W e. LVec )
29 simpl12 
 |-  ( ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) /\ v e. ( K ` G ) ) -> G e. F )
30 simpr 
 |-  ( ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) /\ v e. ( K ` G ) ) -> v e. ( K ` G ) )
31 2 3 5 6 lkrf0 
 |-  ( ( W e. LVec /\ G e. F /\ v e. ( K ` G ) ) -> ( G ` v ) = .0. )
32 28 29 30 31 syl3anc 
 |-  ( ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) /\ v e. ( K ` G ) ) -> ( G ` v ) = .0. )
33 32 ex 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( v e. ( K ` G ) -> ( G ` v ) = .0. ) )
34 33 necon3ad 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( ( G ` v ) =/= .0. -> -. v e. ( K ` G ) ) )
35 27 34 mpd 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> -. v e. ( K ` G ) )
36 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
37 1 36 5 6 lkrlsp3 
 |-  ( ( W e. LVec /\ ( v e. V /\ G e. F ) /\ -. v e. ( K ` G ) ) -> ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V )
38 20 21 22 35 37 syl121anc 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V /\ ( G ` v ) = ( 1r ` D ) ) -> ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V )
39 38 3expia 
 |-  ( ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) /\ v e. V ) -> ( ( G ` v ) = ( 1r ` D ) -> ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V ) )
40 39 reximdva 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( E. v e. V ( G ` v ) = ( 1r ` D ) -> E. v e. V ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V ) )
41 19 40 mpd 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. v e. V ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V )
42 1 36 10 4 islshp 
 |-  ( W e. LVec -> ( ( K ` G ) e. H <-> ( ( K ` G ) e. ( LSubSp ` W ) /\ ( K ` G ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V ) ) )
43 42 3ad2ant1 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( ( K ` G ) e. H <-> ( ( K ` G ) e. ( LSubSp ` W ) /\ ( K ` G ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` G ) u. { v } ) ) = V ) ) )
44 12 17 41 43 mpbir3and 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( K ` G ) e. H )