Metamath Proof Explorer

Theorem lcfrlem5

Description: Lemma for lcfr . The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 lcfrlem5.h 
 |-  H = ( LHyp ` K )
2 lcfrlem5.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrlem5.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrlem5.v 
 |-  V = ( Base ` U )
5 lcfrlem5.f 
 |-  F = ( LFnl ` U )
6 lcfrlem5.l 
 |-  L = ( LKer ` U )
7 lcfrlem5.d 
 |-  D = ( LDual ` U )
8 lcfrlem5.s 
 |-  S = ( LSubSp ` D )
9 lcfrlem5.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcfrlem5.r 
 |-  ( ph -> R e. S )
11 lcfrlem5.q 
 |-  Q = U_ f e. R ( ._|_ ` ( L ` f ) )
12 lcfrlem5.x 
 |-  ( ph -> X e. Q )
13 lcfrlem5.c 
 |-  C = ( Scalar ` U )
14 lcfrlem5.b 
 |-  B = ( Base ` C )
15 lcfrlem5.t 
 |-  .x. = ( .s ` U )
16 lcfrlem5.a 
 |-  ( ph -> A e. B )
17 12 11 eleqtrdi 
 |-  ( ph -> X e. U_ f e. R ( ._|_ ` ( L ` f ) ) )
18 eliun 
 |-  ( X e. U_ f e. R ( ._|_ ` ( L ` f ) ) <-> E. f e. R X e. ( ._|_ ` ( L ` f ) ) )
19 17 18 sylib 
 |-  ( ph -> E. f e. R X e. ( ._|_ ` ( L ` f ) ) )
20 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
21 20 ad2antrr 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> U e. LMod )
22 9 ad2antrr 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> ( K e. HL /\ W e. H ) )
23 eqid 
 |-  ( Base ` D ) = ( Base ` D )
24 23 8 lssss 
 |-  ( R e. S -> R C_ ( Base ` D ) )
25 10 24 syl 
 |-  ( ph -> R C_ ( Base ` D ) )
26 5 7 23 20 ldualvbase 
 |-  ( ph -> ( Base ` D ) = F )
27 25 26 sseqtrd 
 |-  ( ph -> R C_ F )
28 27 sselda 
 |-  ( ( ph /\ f e. R ) -> f e. F )
29 28 adantr 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> f e. F )
30 4 5 6 21 29 lkrssv 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> ( L ` f ) C_ V )
31 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
32 1 3 4 31 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` f ) C_ V ) -> ( ._|_ ` ( L ` f ) ) e. ( LSubSp ` U ) )
33 22 30 32 syl2anc 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> ( ._|_ ` ( L ` f ) ) e. ( LSubSp ` U ) )
34 16 ad2antrr 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> A e. B )
35 simpr 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> X e. ( ._|_ ` ( L ` f ) ) )
36 13 15 14 31 lssvscl 
 |-  ( ( ( U e. LMod /\ ( ._|_ ` ( L ` f ) ) e. ( LSubSp ` U ) ) /\ ( A e. B /\ X e. ( ._|_ ` ( L ` f ) ) ) ) -> ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) )
37 21 33 34 35 36 syl22anc 
 |-  ( ( ( ph /\ f e. R ) /\ X e. ( ._|_ ` ( L ` f ) ) ) -> ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) )
38 37 ex 
 |-  ( ( ph /\ f e. R ) -> ( X e. ( ._|_ ` ( L ` f ) ) -> ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) ) )
39 38 reximdva 
 |-  ( ph -> ( E. f e. R X e. ( ._|_ ` ( L ` f ) ) -> E. f e. R ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) ) )
40 19 39 mpd 
 |-  ( ph -> E. f e. R ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) )
41 eliun 
 |-  ( ( A .x. X ) e. U_ f e. R ( ._|_ ` ( L ` f ) ) <-> E. f e. R ( A .x. X ) e. ( ._|_ ` ( L ` f ) ) )
42 40 41 sylibr 
 |-  ( ph -> ( A .x. X ) e. U_ f e. R ( ._|_ ` ( L ` f ) ) )
43 42 11 eleqtrrdi 
 |-  ( ph -> ( A .x. X ) e. Q )