Metamath Proof Explorer

Theorem lcfl6lem

Description: Lemma for lcfl6 . A functional G (whose kernel is closed by dochsnkr ) is comletely determined by a vector X in the orthocomplement in its kernel at which the functional value is 1. Note that the \ { .0. } in the X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lcfl6lem.h 
 |-  H = ( LHyp ` K )
2 lcfl6lem.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl6lem.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl6lem.v 
 |-  V = ( Base ` U )
5 lcfl6lem.a 
 |-  .+ = ( +g ` U )
6 lcfl6lem.t 
 |-  .x. = ( .s ` U )
7 lcfl6lem.s 
 |-  S = ( Scalar ` U )
8 lcfl6lem.i 
 |-  .1. = ( 1r ` S )
9 lcfl6lem.r 
 |-  R = ( Base ` S )
10 lcfl6lem.z 
 |-  .0. = ( 0g ` U )
11 lcfl6lem.f 
 |-  F = ( LFnl ` U )
12 lcfl6lem.l 
 |-  L = ( LKer ` U )
13 lcfl6lem.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
14 lcfl6lem.g 
 |-  ( ph -> G e. F )
15 lcfl6lem.x 
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
16 lcfl6lem.y 
 |-  ( ph -> ( G ` X ) = .1. )
17 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
18 1 3 13 dvhlvec 
 |-  ( ph -> U e. LVec )
19 1 3 13 dvhlmod 
 |-  ( ph -> U e. LMod )
20 4 11 12 19 14 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
21 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
22 13 20 21 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
23 15 eldifad 
 |-  ( ph -> X e. ( ._|_ ` ( L ` G ) ) )
24 22 23 sseldd 
 |-  ( ph -> X e. V )
25 eqid 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
26 eldifsni 
 |-  ( X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) -> X =/= .0. )
27 15 26 syl 
 |-  ( ph -> X =/= .0. )
28 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
29 24 27 28 sylanbrc 
 |-  ( ph -> X e. ( V \ { .0. } ) )
30 1 2 3 4 10 5 6 11 7 9 25 13 29 dochflcl 
 |-  ( ph -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) e. F )
31 1 2 3 4 10 11 12 13 14 15 dochsnkr 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { X } ) )
32 1 2 3 4 10 5 6 12 7 9 25 13 29 dochsnkr2 
 |-  ( ph -> ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) ) = ( ._|_ ` { X } ) )
33 31 32 eqtr4d 
 |-  ( ph -> ( L ` G ) = ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) ) )
34 1 2 3 4 5 6 10 7 9 8 13 29 25 dochfl1 
 |-  ( ph -> ( ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) ` X ) = .1. )
35 16 34 eqtr4d 
 |-  ( ph -> ( G ` X ) = ( ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) ` X ) )
36 1 2 3 4 7 17 10 11 12 13 14 15 dochfln0 
 |-  ( ph -> ( G ` X ) =/= ( 0g ` S ) )
37 4 7 9 17 11 12 18 24 14 30 33 35 36 eqlkr3 
 |-  ( ph -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) ) )