Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lkrshp Structured version   Unicode version

Theorem lkrshp 29840
 Description: The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.)
Hypotheses
Ref Expression
lkrshp.v
lkrshp.d Scalar
lkrshp.z
lkrshp.h LSHyp
lkrshp.f LFnl
lkrshp.k LKer
Assertion
Ref Expression
lkrshp

Proof of Theorem lkrshp
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 lveclmod 16170 . . . 4
3 simp2 958 . . 3
4 lkrshp.f . . . 4 LFnl
5 lkrshp.k . . . 4 LKer
6 eqid 2435 . . . 4
74, 5, 6lkrlss 29830 . . 3
82, 3, 7syl2anc 643 . 2
9 simp3 959 . . 3
10 lkrshp.d . . . . . 6 Scalar
11 lkrshp.z . . . . . 6
12 lkrshp.v . . . . . 6
1310, 11, 12, 4, 5lkr0f 29829 . . . . 5
142, 3, 13syl2anc 643 . . . 4
1514necon3bid 2633 . . 3
169, 15mpbird 224 . 2
17 eqid 2435 . . . 4
1810, 11, 17, 12, 4lfl1 29805 . . 3
19 simp11 987 . . . . . 6
20 simp2 958 . . . . . 6
21 simp12 988 . . . . . 6
22 simp3 959 . . . . . . . 8
2310lvecdrng 16169 . . . . . . . . 9
2411, 17drngunz 15842 . . . . . . . . 9
2519, 23, 243syl 19 . . . . . . . 8
2622, 25eqnetrd 2616 . . . . . . 7
27 simpl11 1032 . . . . . . . . . 10
28 simpl12 1033 . . . . . . . . . 10
29 simpr 448 . . . . . . . . . 10
3010, 11, 4, 5lkrf0 29828 . . . . . . . . . 10
3127, 28, 29, 30syl3anc 1184 . . . . . . . . 9
3231ex 424 . . . . . . . 8
3332necon3ad 2634 . . . . . . 7
3426, 33mpd 15 . . . . . 6
35 eqid 2435 . . . . . . 7
3612, 35, 4, 5lkrlsp3 29839 . . . . . 6
3719, 20, 21, 34, 36syl121anc 1189 . . . . 5
38373expia 1155 . . . 4
3938reximdva 2810 . . 3
4018, 39mpd 15 . 2
41 lkrshp.h . . . 4 LSHyp
4212, 35, 6, 41islshp 29714 . . 3