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 )