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=BaseU
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=BaseU
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 biimtrid ⊢φ→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