Metamath Proof Explorer

Theorem lkrshpor

Description: The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 lkrshpor.v ⊢ V = Base W
2 lkrshpor.h ⊢ H = LSHyp ⁡ W
3 lkrshpor.f ⊢ F = LFnl ⁡ W
4 lkrshpor.k ⊢ K = LKer ⁡ W
5 lkrshpor.w ⊢ φ → W ∈ LVec
6 lkrshpor.g ⊢ φ → G ∈ F
7 lveclmod ⊢ W ∈ LVec → W ∈ LMod
8 5 7 syl ⊢ φ → W ∈ LMod
9 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
10 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
11 9 10 1 3 4 lkr0f ⊢ W ∈ LMod ∧ G ∈ F → K ⁡ G = V ↔ G = V × 0 Scalar ⁡ W
12 8 6 11 syl2anc ⊢ φ → K ⁡ G = V ↔ G = V × 0 Scalar ⁡ W
13 12 biimpar ⊢ φ ∧ G = V × 0 Scalar ⁡ W → K ⁡ G = V
14 13 olcd ⊢ φ ∧ G = V × 0 Scalar ⁡ W → K ⁡ G ∈ H ∨ K ⁡ G = V
15 5 adantr ⊢ φ ∧ G ≠ V × 0 Scalar ⁡ W → W ∈ LVec
16 6 adantr ⊢ φ ∧ G ≠ V × 0 Scalar ⁡ W → G ∈ F
17 simpr ⊢ φ ∧ G ≠ V × 0 Scalar ⁡ W → G ≠ V × 0 Scalar ⁡ W
18 1 9 10 2 3 4 lkrshp ⊢ W ∈ LVec ∧ G ∈ F ∧ G ≠ V × 0 Scalar ⁡ W → K ⁡ G ∈ H
19 15 16 17 18 syl3anc ⊢ φ ∧ G ≠ V × 0 Scalar ⁡ W → K ⁡ G ∈ H
20 19 orcd ⊢ φ ∧ G ≠ V × 0 Scalar ⁡ W → K ⁡ G ∈ H ∨ K ⁡ G = V
21 14 20 pm2.61dane ⊢ φ → K ⁡ G ∈ H ∨ K ⁡ G = V