Metamath Proof Explorer

Theorem dochsnkr2cl

Description: The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015)

Ref Expression
Hypotheses dochsnkr2.h 
|- H = ( LHyp ` K )
dochsnkr2.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochsnkr2.u 
|- U = ( ( DVecH ` K ) ` W )
dochsnkr2.v 
|- V = ( Base ` U )
dochsnkr2.z 
|- .0. = ( 0g ` U )
dochsnkr2.a 
|- .+ = ( +g ` U )
dochsnkr2.t 
|- .x. = ( .s ` U )
dochsnkr2.l 
|- L = ( LKer ` U )
dochsnkr2.d 
|- D = ( Scalar ` U )
dochsnkr2.r 
|- R = ( Base ` D )
dochsnkr2.g 
|- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
dochsnkr2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochsnkr2.x 
|- ( ph -> X e. ( V \ { .0. } ) )
Assertion dochsnkr2cl 
|- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )

Proof

Step Hyp Ref Expression
1 dochsnkr2.h 
 |-  H = ( LHyp ` K )
2 dochsnkr2.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochsnkr2.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochsnkr2.v 
 |-  V = ( Base ` U )
5 dochsnkr2.z 
 |-  .0. = ( 0g ` U )
6 dochsnkr2.a 
 |-  .+ = ( +g ` U )
7 dochsnkr2.t 
 |-  .x. = ( .s ` U )
8 dochsnkr2.l 
 |-  L = ( LKer ` U )
9 dochsnkr2.d 
 |-  D = ( Scalar ` U )
10 dochsnkr2.r 
 |-  R = ( Base ` D )
11 dochsnkr2.g 
 |-  G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
12 dochsnkr2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 dochsnkr2.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
14 1 3 12 dvhlmod 
 |-  ( ph -> U e. LMod )
15 13 eldifad 
 |-  ( ph -> X e. V )
16 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
17 4 16 lspsnid 
 |-  ( ( U e. LMod /\ X e. V ) -> X e. ( ( LSpan ` U ) ` { X } ) )
18 14 15 17 syl2anc 
 |-  ( ph -> X e. ( ( LSpan ` U ) ` { X } ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 dochsnkr2 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )
20 15 snssd 
 |-  ( ph -> { X } C_ V )
21 1 3 2 4 16 12 20 dochocsp 
 |-  ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
22 19 21 eqtr4d 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) )
23 22 fveq2d 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) ) )
24 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
25 1 3 4 16 24 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( ( LSpan ` U ) ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
26 12 15 25 syl2anc 
 |-  ( ph -> ( ( LSpan ` U ) ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
27 1 24 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( LSpan ` U ) ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) ) = ( ( LSpan ` U ) ` { X } ) )
28 12 26 27 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) ) = ( ( LSpan ` U ) ` { X } ) )
29 23 28 eqtr2d 
 |-  ( ph -> ( ( LSpan ` U ) ` { X } ) = ( ._|_ ` ( L ` G ) ) )
30 18 29 eleqtrd 
 |-  ( ph -> X e. ( ._|_ ` ( L ` G ) ) )
31 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
32 13 31 syl 
 |-  ( ph -> X =/= .0. )
33 eldifsn 
 |-  ( X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) <-> ( X e. ( ._|_ ` ( L ` G ) ) /\ X =/= .0. ) )
34 30 32 33 sylanbrc 
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )