Metamath Proof Explorer

Theorem dochsnkr

Description: A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h 
|- H = ( LHyp ` K )
dochsnkr.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochsnkr.u 
|- U = ( ( DVecH ` K ) ` W )
dochsnkr.v 
|- V = ( Base ` U )
dochsnkr.z 
|- .0. = ( 0g ` U )
dochsnkr.f 
|- F = ( LFnl ` U )
dochsnkr.l 
|- L = ( LKer ` U )
dochsnkr.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochsnkr.g 
|- ( ph -> G e. F )
dochsnkr.x 
|- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
Assertion dochsnkr 
|- ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )

Proof

Step Hyp Ref Expression
1 dochsnkr.h 
 |-  H = ( LHyp ` K )
2 dochsnkr.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochsnkr.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochsnkr.v 
 |-  V = ( Base ` U )
5 dochsnkr.z 
 |-  .0. = ( 0g ` U )
6 dochsnkr.f 
 |-  F = ( LFnl ` U )
7 dochsnkr.l 
 |-  L = ( LKer ` U )
8 dochsnkr.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dochsnkr.g 
 |-  ( ph -> G e. F )
10 dochsnkr.x 
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
11 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
12 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
13 1 3 8 dvhlvec 
 |-  ( ph -> U e. LVec )
14 1 2 3 4 5 6 7 8 9 10 12 dochsnkrlem2 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) )
15 10 eldifad 
 |-  ( ph -> X e. ( ._|_ ` ( L ` G ) ) )
16 eldifsni 
 |-  ( X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) -> X =/= .0. )
17 10 16 syl 
 |-  ( ph -> X =/= .0. )
18 5 11 12 13 14 15 17 lsatel 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { X } ) )
19 18 fveq2d 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) )
20 1 2 3 4 5 6 7 8 9 10 dochsnkrlem3 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
21 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
22 4 6 7 21 9 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
23 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
24 8 22 23 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
25 24 ssdifssd 
 |-  ( ph -> ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) C_ V )
26 25 10 sseldd 
 |-  ( ph -> X e. V )
27 26 snssd 
 |-  ( ph -> { X } C_ V )
28 1 3 2 4 11 8 27 dochocsp 
 |-  ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
29 19 20 28 3eqtr3d 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )