Metamath Proof Explorer

Theorem lclkrslem1

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses lclkrslem1.h 
|- H = ( LHyp ` K )
lclkrslem1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrslem1.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrslem1.s 
|- S = ( LSubSp ` U )
lclkrslem1.f 
|- F = ( LFnl ` U )
lclkrslem1.l 
|- L = ( LKer ` U )
lclkrslem1.d 
|- D = ( LDual ` U )
lclkrslem1.r 
|- R = ( Scalar ` U )
lclkrslem1.b 
|- B = ( Base ` R )
lclkrslem1.t 
|- .x. = ( .s ` D )
lclkrslem1.c 
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
lclkrslem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrslem1.q 
|- ( ph -> Q e. S )
lclkrslem1.g 
|- ( ph -> G e. C )
lclkrslem1.x 
|- ( ph -> X e. B )
Assertion lclkrslem1 
|- ( ph -> ( X .x. G ) e. C )

Proof

Step Hyp Ref Expression
1 lclkrslem1.h 
 |-  H = ( LHyp ` K )
2 lclkrslem1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrslem1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrslem1.s 
 |-  S = ( LSubSp ` U )
5 lclkrslem1.f 
 |-  F = ( LFnl ` U )
6 lclkrslem1.l 
 |-  L = ( LKer ` U )
7 lclkrslem1.d 
 |-  D = ( LDual ` U )
8 lclkrslem1.r 
 |-  R = ( Scalar ` U )
9 lclkrslem1.b 
 |-  B = ( Base ` R )
10 lclkrslem1.t 
 |-  .x. = ( .s ` D )
11 lclkrslem1.c 
 |-  C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
12 lclkrslem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 lclkrslem1.q 
 |-  ( ph -> Q e. S )
14 lclkrslem1.g 
 |-  ( ph -> G e. C )
15 lclkrslem1.x 
 |-  ( ph -> X e. B )
16 eqid 
 |-  { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
17 11 16 lcfls1c 
 |-  ( G e. C <-> ( G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
18 17 simplbi 
 |-  ( G e. C -> G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
19 14 18 syl 
 |-  ( ph -> G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
20 1 2 3 5 6 7 8 9 10 16 12 15 19 lclkrlem1 
 |-  ( ph -> ( X .x. G ) e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
21 eqid 
 |-  ( Base ` U ) = ( Base ` U )
22 1 3 12 dvhlmod 
 |-  ( ph -> U e. LMod )
23 11 lcfls1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
24 14 23 sylib 
 |-  ( ph -> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
25 24 simp1d 
 |-  ( ph -> G e. F )
26 5 8 9 7 10 22 15 25 ldualvscl 
 |-  ( ph -> ( X .x. G ) e. F )
27 21 5 6 22 26 lkrssv 
 |-  ( ph -> ( L ` ( X .x. G ) ) C_ ( Base ` U ) )
28 1 3 12 dvhlvec 
 |-  ( ph -> U e. LVec )
29 8 9 5 6 7 10 28 25 15 lkrss 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( X .x. G ) ) )
30 1 3 21 2 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` ( X .x. G ) ) C_ ( Base ` U ) /\ ( L ` G ) C_ ( L ` ( X .x. G ) ) ) -> ( ._|_ ` ( L ` ( X .x. G ) ) ) C_ ( ._|_ ` ( L ` G ) ) )
31 12 27 29 30 syl3anc 
 |-  ( ph -> ( ._|_ ` ( L ` ( X .x. G ) ) ) C_ ( ._|_ ` ( L ` G ) ) )
32 24 simp3d 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ Q )
33 31 32 sstrd 
 |-  ( ph -> ( ._|_ ` ( L ` ( X .x. G ) ) ) C_ Q )
34 11 16 lcfls1c 
 |-  ( ( X .x. G ) e. C <-> ( ( X .x. G ) e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } /\ ( ._|_ ` ( L ` ( X .x. G ) ) ) C_ Q ) )
35 20 33 34 sylanbrc 
 |-  ( ph -> ( X .x. G ) e. C )