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 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochkrshp.g 
|- ( ph -> G e. F )
Assertion dochkrshp 
|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. 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 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dochkrshp.g 
 |-  ( ph -> G e. F )
10 simpr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) )
11 8 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) ) -> ( K e. HL /\ W e. H ) )
12 2fveq3 
 |-  ( ( L ` G ) = V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
13 1 3 2 4 8 dochoc1 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )
14 12 13 sylan9eqr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = V )
15 simpr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` G ) = V )
16 14 15 eqtr4d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
17 16 ex 
 |-  ( ph -> ( ( L ` G ) = V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
18 17 necon3d 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) -> ( L ` G ) =/= V ) )
19 df-ne 
 |-  ( ( L ` G ) =/= V <-> -. ( L ` G ) = V )
20 1 3 8 dvhlvec 
 |-  ( ph -> U e. LVec )
21 4 5 6 7 20 9 lkrshpor 
 |-  ( ph -> ( ( L ` G ) e. Y \/ ( L ` G ) = V ) )
22 21 orcomd 
 |-  ( ph -> ( ( L ` G ) = V \/ ( L ` G ) e. Y ) )
23 22 ord 
 |-  ( ph -> ( -. ( L ` G ) = V -> ( L ` G ) e. Y ) )
24 19 23 syl5bi 
 |-  ( ph -> ( ( L ` G ) =/= V -> ( L ` G ) e. Y ) )
25 18 24 syld 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) -> ( L ` G ) e. Y ) )
26 25 imp 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) ) -> ( L ` G ) e. Y )
27 1 2 3 4 5 11 26 dochshpncl 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) ) -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = V ) )
28 10 27 mpbid 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = V )
29 28 ex 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= ( L ` G ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = V ) )
30 29 necon1d 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
31 14 ex 
 |-  ( ph -> ( ( L ` G ) = V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = V ) )
32 31 necon3ad 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V -> -. ( L ` G ) = V ) )
33 32 23 syld 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V -> ( L ` G ) e. Y ) )
34 30 33 jcad 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( L ` G ) e. Y ) ) )
35 1 2 3 6 5 7 8 9 dochlkr 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( L ` G ) e. Y ) ) )
36 34 35 sylibrd 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) )
37 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
38 37 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) -> U e. LMod )
39 simpr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y )
40 4 5 38 39 lshpne 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
41 40 ex 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )
42 36 41 impbid 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) e. Y ) )