Metamath Proof Explorer


Theorem dochkrshp

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

Ref Expression
Hypotheses dochkrshp.h H = LHyp K
dochkrshp.o ˙ = ocH K W
dochkrshp.u U = DVecH K W
dochkrshp.v V = Base U
dochkrshp.y Y = LSHyp U
dochkrshp.f F = LFnl U
dochkrshp.l L = LKer U
dochkrshp.k φ K HL W H
dochkrshp.g φ G F
Assertion dochkrshp φ ˙ ˙ L G V ˙ ˙ L G Y

Proof

Step Hyp Ref Expression
1 dochkrshp.h H = LHyp K
2 dochkrshp.o ˙ = ocH K W
3 dochkrshp.u U = DVecH K W
4 dochkrshp.v V = Base U
5 dochkrshp.y Y = LSHyp U
6 dochkrshp.f F = LFnl U
7 dochkrshp.l L = LKer U
8 dochkrshp.k φ K HL W H
9 dochkrshp.g φ G F
10 simpr φ ˙ ˙ L G L G ˙ ˙ L G L G
11 8 adantr φ ˙ ˙ L G L G K HL W H
12 2fveq3 L G = V ˙ ˙ L G = ˙ ˙ V
13 1 3 2 4 8 dochoc1 φ ˙ ˙ V = V
14 12 13 sylan9eqr φ L G = V ˙ ˙ L G = V
15 simpr φ L G = V L G = V
16 14 15 eqtr4d φ L G = V ˙ ˙ L G = L G
17 16 ex φ L G = V ˙ ˙ L G = L G
18 17 necon3d φ ˙ ˙ L G L G L G V
19 df-ne L G V ¬ L G = V
20 1 3 8 dvhlvec φ U LVec
21 4 5 6 7 20 9 lkrshpor φ L G Y L G = V
22 21 orcomd φ L G = V L G Y
23 22 ord φ ¬ L G = V L G Y
24 19 23 syl5bi φ L G V L G Y
25 18 24 syld φ ˙ ˙ L G L G L G Y
26 25 imp φ ˙ ˙ L G L G L G Y
27 1 2 3 4 5 11 26 dochshpncl φ ˙ ˙ L G L G ˙ ˙ L G L G ˙ ˙ L G = V
28 10 27 mpbid φ ˙ ˙ L G L G ˙ ˙ L G = V
29 28 ex φ ˙ ˙ L G L G ˙ ˙ L G = V
30 29 necon1d φ ˙ ˙ L G V ˙ ˙ L G = L G
31 14 ex φ L G = V ˙ ˙ L G = V
32 31 necon3ad φ ˙ ˙ L G V ¬ L G = V
33 32 23 syld φ ˙ ˙ L G V L G Y
34 30 33 jcad φ ˙ ˙ L G V ˙ ˙ L G = L G L G Y
35 1 2 3 6 5 7 8 9 dochlkr φ ˙ ˙ L G Y ˙ ˙ L G = L G L G Y
36 34 35 sylibrd φ ˙ ˙ L G V ˙ ˙ L G Y
37 1 3 8 dvhlmod φ U LMod
38 37 adantr φ ˙ ˙ L G Y U LMod
39 simpr φ ˙ ˙ L G Y ˙ ˙ L G Y
40 4 5 38 39 lshpne φ ˙ ˙ L G Y ˙ ˙ L G V
41 40 ex φ ˙ ˙ L G Y ˙ ˙ L G V
42 36 41 impbid φ ˙ ˙ L G V ˙ ˙ L G Y