Metamath Proof Explorer

Theorem lkrshp4

Description: A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014)

Ref Expression
Hypotheses lkrshp4.v ⊢ V = Base W
lkrshp4.h ⊢ H = LSHyp ⁡ W
lkrshp4.f ⊢ F = LFnl ⁡ W
lkrshp4.k ⊢ K = LKer ⁡ W
lkrshp4.w ⊢ φ → W ∈ LVec
lkrshp4.g ⊢ φ → G ∈ F
Assertion lkrshp4 ⊢ φ → K ⁡ G ≠ V ↔ K ⁡ G ∈ H

Proof

Step Hyp Ref Expression
1 lkrshp4.v ⊢ V = Base W
2 lkrshp4.h ⊢ H = LSHyp ⁡ W
3 lkrshp4.f ⊢ F = LFnl ⁡ W
4 lkrshp4.k ⊢ K = LKer ⁡ W
5 lkrshp4.w ⊢ φ → W ∈ LVec
6 lkrshp4.g ⊢ φ → G ∈ F
7 1 2 3 4 5 6 lkrshpor ⊢ φ → K ⁡ G ∈ H ∨ K ⁡ G = V
8 7 orcomd ⊢ φ → K ⁡ G = V ∨ K ⁡ G ∈ H
9 neor ⊢ K ⁡ G = V ∨ K ⁡ G ∈ H ↔ K ⁡ G ≠ V → K ⁡ G ∈ H
10 8 9 sylib ⊢ φ → K ⁡ G ≠ V → K ⁡ G ∈ H
11 lveclmod ⊢ W ∈ LVec → W ∈ LMod
12 5 11 syl ⊢ φ → W ∈ LMod
13 12 adantr ⊢ φ ∧ K ⁡ G ∈ H → W ∈ LMod
14 simpr ⊢ φ ∧ K ⁡ G ∈ H → K ⁡ G ∈ H
15 1 2 13 14 lshpne ⊢ φ ∧ K ⁡ G ∈ H → K ⁡ G ≠ V
16 15 ex ⊢ φ → K ⁡ G ∈ H → K ⁡ G ≠ V
17 10 16 impbid ⊢ φ → K ⁡ G ≠ V ↔ K ⁡ G ∈ H