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