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 ˙ = 0 D
lkrshp3.h H = LSHyp W
lkrshp3.f F = LFnl W
lkrshp3.k K = LKer W
lkrshp3.w φ W LVec
lkrshp3.g φ G F
Assertion lkrshp3 φ K G H G V × 0 ˙

Proof

Step Hyp Ref Expression
1 lkrshp3.v V = Base W
2 lkrshp3.d D = Scalar W
3 lkrshp3.o 0 ˙ = 0 D
4 lkrshp3.h H = LSHyp W
5 lkrshp3.f F = LFnl W
6 lkrshp3.k K = LKer W
7 lkrshp3.w φ W LVec
8 lkrshp3.g φ G F
9 lveclmod W LVec W LMod
10 7 9 syl φ W LMod
11 10 adantr φ K G H W LMod
12 simpr φ K G H K G H
13 1 4 11 12 lshpne φ K G H K G V
14 2 3 1 5 6 lkr0f W LMod G F K G = V G = V × 0 ˙
15 10 8 14 syl2anc φ K G = V G = V × 0 ˙
16 15 adantr φ K G H K G = V G = V × 0 ˙
17 16 necon3bid φ K G H K G V G V × 0 ˙
18 13 17 mpbid φ K G H G V × 0 ˙
19 7 adantr φ G V × 0 ˙ W LVec
20 8 adantr φ G V × 0 ˙ G F
21 simpr φ G V × 0 ˙ G V × 0 ˙
22 1 2 3 4 5 6 lkrshp W LVec G F G V × 0 ˙ K G H
23 19 20 21 22 syl3anc φ G V × 0 ˙ K G H
24 18 23 impbida φ K G H G V × 0 ˙