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 ˙ = 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 ˙