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=BaseW
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=BaseW
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 ⊢0Scalar⁡W=0Scalar⁡W
11 9 10 1 3 4 lkr0f ⊢W∈LMod∧G∈F→K⁡G=V↔G=V×0Scalar⁡W
12 8 6 11 syl2anc ⊢φ→K⁡G=V↔G=V×0Scalar⁡W
13 12 biimpar ⊢φ∧G=V×0Scalar⁡W→K⁡G=V
14 13 olcd ⊢φ∧G=V×0Scalar⁡W→K⁡G∈H∨K⁡G=V
15 5 adantr ⊢φ∧G≠V×0Scalar⁡W→W∈LVec
16 6 adantr ⊢φ∧G≠V×0Scalar⁡W→G∈F
17 simpr ⊢φ∧G≠V×0Scalar⁡W→G≠V×0Scalar⁡W
18 1 9 10 2 3 4 lkrshp ⊢W∈LVec∧G∈F∧G≠V×0Scalar⁡W→K⁡G∈H
19 15 16 17 18 syl3anc ⊢φ∧G≠V×0Scalar⁡W→K⁡G∈H
20 19 orcd ⊢φ∧G≠V×0Scalar⁡W→K⁡G∈H∨K⁡G=V
21 14 20 pm2.61dane ⊢φ→K⁡G∈H∨K⁡G=V